How does ZF set theory prevent Russell's Paradox In chapter 1 § 5 of Set theory by Kenneth Kunen. Kunnen explains that a naive attempt for formalizing Axiom of Comprehension would look like $\exists y \forall x (x \in y \leftrightarrow \phi)$.
But the book claim it is incorrect because when we define $\phi$ as $x \notin x$ we can have the following deduction $\forall x (x \in y \leftrightarrow x \notin x)$,And when $x = y$ we get $(y \in y \leftrightarrow y \notin y)$.
So instead the book suggests the correct Axiom to be $\exists y \forall x (x \in y \leftrightarrow x \in z \wedge \phi)$.
But when I tried following the exact same step I ended up with $(y \in y \leftrightarrow y \in z \wedge y \notin y)$.
If $y \in z$ evaluated to true, we will end with the exact same predicate as with the naive Axiom of comprehension. I know that Russell's paradox should not work in ZF set theory, but I cannot figure out what is wrong with my reasoning.
 A: I think there is a flaw in my my proof and when I tried to write the proof formally I think I was able to see why the paradox does not hold.
The proof is Gentzen style (which the book does not use) and it was the only way I was able to follow.
The Full Axiom of Comprehension says that: For each formula $\phi$ with free variables among $x, y, z, w_1, ..., w_n$
$$
\forall z \forall w_1, ..., w_n\exists y \forall x (x\in y \leftrightarrow x \in z \wedge \phi)
$$
We assume $\phi$ is $x \notin x$ so we no longer need $w_1,....w_n$
The proof will look like following:
$$
\dfrac
{
\dfrac{
\dfrac{
\dfrac{
\dfrac{
\dfrac{}{z, x, x \in z \vdash x \in z \wedge x \notin x}\text{*}
}
{z, x \vdash (x\in z \rightarrow x \in z \wedge x \notin x)}
~~~~~~~
\dfrac{
\dfrac{}{z, x, x \in z, x \notin x \vdash x \in z}(assumptions)}
{z, x \vdash x \in z \wedge x \notin x \rightarrow x \in z} (\text{introuce the hypothesis})
}{
z, x \vdash x\in z \leftrightarrow x \in z \wedge x \notin x
}(\text{split equivalence})}{z \vdash \forall x (x\in z \leftrightarrow x \in z \wedge x \notin x)} ( \text{introduce } x)
}
{z \vdash \exists y \forall x (x\in y \leftrightarrow x \in z \wedge x \notin x)} (\text{exists }z)
}
{\vdash\forall z \exists y \forall x (x\in y \leftrightarrow x \in z \wedge x \notin x) } (\text{introduce } z)
$$
The continuation of proof of * is:
1- Proving that $z, x, x \in z \vdash x \in z$ which is trivial by assumptions.
2- Proving that $z, x, x \in z \vdash x \notin x$. which is the same as
$z, x, x \in z, x \in x \vdash false$. I struggled there for a bit but I learned that this is a direct consequence from Foundational Axiom which will be discussed later in chapter 3.
