I'm attempting to learn Set Theory and I'm currently working through Halmos' Naive Set Theory. I will say that I completely understand the essence of the Axiom of Extensionality. However, where I'm stumbling is grasping its formalization in set-builder notation. So, looking at: $\forall x\forall y \, \left(x=y \leftrightarrow \forall z \, \left(z\in x \leftrightarrow z\in y\right)\right)$
The part I do not follow is the $\left(z\in x\leftrightarrow z\in y\right)$
So, in my head, if I imagine that I have a set $x$ that is $\{ “a”, “b”, “c”\}$ and I have a set $y$ that is $\{“a”, “b”, “c”, “d” \}$, I intuitively understand that by the Axiom of Extension, sets $x$ and $y$ are not equal. However, I don't follow how the formal statement would yield this. So for example, suppose we have a set $z$ that is $\{ “a”, “b”, “c”\}$.
So, in my mind - here's what I do to mentally work through the formal statement of the axiom. First, I'll ask myself: Is $z$ in $y$? Well, since $y$ is $a, b, c, d$ and $z$ is $a, b, c$ - so it would certainly seem that $z$ is in fact in $y$. So then I'll ask myself: Is $z$ in $x$? Well, $x$ is $a, b, c$ and $z$ is $a, b, c$ - so it would certainly seem that $z$ is also in fact in $x$! Therefore, the expression $\left(z \in x \leftrightarrow z \in y\right)$ should evaluate to True and therefore $x = y$ (which of course I know is wrong).
So, hopefully you can see why I am stuck on this. I assume the root of my misunderstanding is a flaw in how I'm interpreting the formal statement; specifically the iff biconditional connective; but I'm just not seeing how/why I am.
Any help in providing clarity on where / how I'm stumbling on this would be greatly appreciated.
Thank you for you time.