Turn set equality into predicate formula

Question

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.

Answer 1

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}$$