Turn set equality into predicate formula

A formula of set theory is a predicate formula that only uses the predicate "$$x \in y$$".

The domain of discourse is the collection of sets, and “$$x \in y$$” is interpreted to mean that the set $$x$$ is one of the elements in the set $$y$$. For example, since $$x$$ and $$y$$ are the same set iff they have the same members, here’s how we can express equality of $$x$$ and $$y$$ with a formula of set theory: $$(x = y) ::= \forall z (z \in x \iff z \in y)$$

Here comes the question. How to write a formula for $$p = \{a, b\}$$.

Here's my solution: $$p = \{a, b\} ::= \forall z \Big((z \ne a \land z \ne b) \implies z \not \in p\Big)$$

Or, should I write it as: $$p = \{a, b\} ::= \forall z \Big((z \ne a \land z \ne b) \iff z \not \in p\Big)$$

Which one is correct? I am very confused right now.

• The second one is quite clear; but why not $\forall z ( z \in p \Leftrightarrow (z=a \lor z=b))$ ? – Mauro ALLEGRANZA Mar 14 at 12:07
• @MauroALLEGRANZA Yeah, that's right! So, you mean my second solution is correct while the first one is wrong? – 王文军 or Wenjun Wang Mar 14 at 12:11
• Contrapose it and what you get is: $z \in p \Rightarrow (z=a \lor z=b)$ – Mauro ALLEGRANZA Mar 14 at 12:20

here’s how we can express equality of $$x$$ and $$y$$ with a formula of set theory: $$\def\iff{\leftrightarrow} (x = y) ::= \forall z (z \in x \iff z \in y)$$
Here comes the question. How to write a formula for $$p = \{a, b\}$$.
Don't reinvent the roundmover™.   Just use substitution. \begin{align}(p = \{a, b\})~::=~&\forall z~(z\in p\iff z\in\{a,b\})\\=~&\forall z~(z\in p\iff (z=a\lor z=b))\\=~&\forall z~(z\in p\iff(\forall y~(y\in z\iff y\in a))\lor( \forall y~(y\in z\iff y\in b)))\end{align}