Does this ordered pair definition imply the axiom of regularity? The axiom of regularity in ZFC states that every non-empty set $S$ has at least one member which is disjoint from $S$. Using the axiom of regularity, we can prove that this alternative definition of ordered pairs $(a,b)= \{a, \{a,b\}\}$ does in fact satisfy the ordered pair characterization. I am now wondering if the converse holds. That is, is there a model of ZFC - Regularity where that construction is an ordered pair function, but the axiom of regularity does not hold?
 A: Note that $\{a,\{a,b\}\}=\{c,\{c,d\}\}$ implies

*

*$a=b$ and $c=d$, or

*$a=\{c,d\}$ and $c=\{a,b\}$ (equivalently, $a=\{\{a,b\},d\}$ and $c=\{a,b\}$), or

*$a=c=\{a,b\}=\{c,d\}$ (equivalent to $a=c$, $b=d$ and $a=\{a,b\}$.)

We can see that regularity excludes the possibility $a=\{\{a,b\},d\}$ or $a=\{a,b\}$. Also, we can see that if there is no such $a$, $b$, $d$, then your definition yields an ordered pair.
Now consider the following: (Exercise IV, #18 of old Kunen.)

Proposition. ($\mathsf{ZFC}$) Let $F:V\to V$ be a one-to-one onto function. Define $E$ such that $a\mathrel{E}b$ iff $x\in F(y)$. Then $(V,E)$ is a model of $\mathsf{ZFC}$ without regularity.

Then consider

*

*$A = \{a_0,a_1,a_2,a_3\}$, where $a_i=i$ for $i<3$, $a_3=\{1\}$.

*$F:V\to V$ such that $F(a_i)=\{a_j\mid j\neq s(i)\}$, $F(\{a_j\mid j\neq i\})=s(i)$, where $s$ is a $4$-cycle, and $F(x)=x$ otherwise.

Then $(V,E)$ violates regularity but $(V,E)$ think there is no $a,b,d$ such that $a=\{\{a,b\},d\}$ or $a=\{a,b\}$: if it happened, then either

*

*there is $a,b$ such that $F(a)=\{a,b\}$, or

*there is $a,b,c,d$ such that $F(a)=\{c,d\}$ and $F(c)=\{a,b\}$,

but we have no such possibilities by definition of $F$.
A: Partial answer:
Work in ZF without regularity. Suppose $\forall a (\forall b \in a (a \notin b))$ [assumption]. It follows that $\forall a (a \notin a)$, since if we had $a \in a$, then we would have $a \in a \in a$ [lemma].
Consider the definition $(a, b) = \{a, \{a, b\}\}$.
Suppose $c, d \in (a, b)$, and suppose that $c \in d$. We have several cases.

*

*$c = a$ and $d = \{a, b\}$. This case works.

*$c = \{a, b\}$ and $d = a$. Then we have $a \in \{a, b\} \in a$, which is ruled out by assumption.

*$c = \{a, b\}$ and $d = \{a, b\}$. Then $\{a, b\} \in \{a, b\}$, which is ruled out by the lemma.

*$c = a$ and $d = a$. Then $a \in a$, so this is ruled out by the lemma.

Then we know that $c = a$ and $d = \{a, b\}$.
Now suppose that $(c, e) = (a, b)$. Then in particular, we have $c, \{c, e\} \in (a, b)$ and $c \in \{c, e\}$. So $c = a$, and $\{c, e\} = \{a, b\}$.
Then $\{a, e\} = \{a, b\}$. Then either $e = a$ or $e = b$. If $e = a$, then either $b = a$, or $b = e$. So in any event, $e = b$.
This proves that $a, b \mapsto (a, b)$ is a pairing function. $\square$
So we need to find some model of ZF without regularity that satisfies our assumption (which is a consequence of regularity in full ZF).
