Defining ordered pairs using only first-order logic The usual definition of an ordered pair $\langle x,y \rangle$ is $\{\{x\},\{x,y\}\}$, but how may one define that using purely first-order logic contructs (variables, logical operations, quantifiers) and the $\in$ relation?
After reading the wiki, which defines the properties:

*

*$x$ is the first coordinate of $p$: $\forall A[A \in p \rightarrow x \in A]$

*$x$ is the second coordinate of $p$: $\exists A[A \in p \land x \in A] \land \forall A \forall B[A \in p \land B \in p \rightarrow (A \neq B \rightarrow x \notin A \lor x \notin B)]$
I arrived at the following definition:
$$
\langle x,y \rangle = p \leftrightarrow \forall A[A \in p \rightarrow x \in A] \land \exists A[A \in p \land y \in A] \land \forall A \forall B[A \in p \land B \in p \rightarrow (A \neq B \rightarrow y \notin A \lor y \notin B)]
$$
However, this definition would also consider $\{\{x\},\{x,y\},\{x,z\}\}$ or $\{\{x\},\{x,y,z\}\}$ as representing that ordered pair, and as such, it is not unique.
So, how may one define ordered pairs using only first-order logic such that only the set $\{\{x\},\{x,y\}\}$ represents the ordered pair $\langle x,y \rangle$?
 A: Here is a more or less mechanical way to do the expansion.  First, $p = \langle x, y \rangle = \{ \{ x \}, \{ x, y \} \}$ is equivalent to:
$$\forall a, a \in p \leftrightarrow (a = \{ x \} \vee a = \{ x, y \}).$$
Now, we can (by manual recursion) replace $a = \{ x \}$ with:
$$\forall b, b \in a \leftrightarrow b = x.$$
Similarly, replace $a = \{ x, y \}$ with:
$$\forall b, b \in a \leftrightarrow (b = x \vee b = y).$$
Therefore, substituting in, we get that $p = \langle x, y \rangle$ is equivalent to:
$$\forall a, a \in p \leftrightarrow [(\forall b, b \in a \leftrightarrow b = x) \vee (\forall b, b \in a \leftrightarrow (b = x \vee b = y))].$$

Note that a generalization of this procedure (formalized) comes up in model theory, under the name of "conversative extension by definition".  (However, in general, in expanding a formula not of the form variable = definition, we might need to introduce some more variables.  For example, if you wanted to expand $\langle x, y \rangle \in z$ instead, then you would first need to expand this to $\exists p, p = \langle x, y \rangle \wedge p \in z$, and then proceed to expand $p = \langle x, y \rangle$ as above.)
A: $p= \langle x, y \rangle \iff \forall z (z \in p \iff \exists w_1 \exists w_2 ((z=w_1 \lor z=w_2) \land ((\forall t_1(t_1 \in w_1 \iff t_1=x)) \land \forall t_2(t_2 \in w_2 \iff (t_2 = x \lor t_2 = y)))).$
Translating this to English, $w_1$ and $w_2$ are the two elements of the set comprising our ordered pair, with $t_1$ as the element of $w_1$ (which we're forcing to be $x$) and $t_2$ as the elements of $w_2$ (which we're forcing to be $x$ or $y$).
