Матлогика. Вывести формулу

[yoba]

Нужно вывести формулу $\exists y \forall z (\forall b (P(b) \leftrightarrow b \in z) \to z \in y)$ при условии $\forall z \neg (P(b) \leftrightarrow b \in z)$.

Из $\forall z \neg (P(b) \leftrightarrow b \in z)$ следует $\neg (P(b) \leftrightarrow b \in z)$.
Т.к. $\neg (P(b) \leftrightarrow b \in z) \to ((P(b) \leftrightarrow b \in z) \to z \in y)$, то $(P(b) \leftrightarrow b \in z) \to z \in y$.
А как дальше, я понять не могу? Какие дальше аксиомы применять?

-- 14.11.2012, 21:11 --

Или может выводимость этой формулы зависит от $P$? Помогите пожалуйста.

P.S. Аксиомы ZFC тоже можно применять.

[yoba]

Забыл про Universal generalization.
Итак, по Universal generalization выводима $\forall z (\forall b (P(b) \leftrightarrow b \in z) \to z \in y)$. И, по одной из аксиом логики предикатов, поэтому выводима $\exists y \forall z (\forall b (P(b) \leftrightarrow b \in z) \to z \in y)$.

Все, тему можно закрывать.