= Solution
Use the <Kuratowski ordered pair>
$$
\langle a,b\rangle=\{\{a\},\{a,b\}\}.
$$
The <axiom of pairing> first produces $\{a\}$ by pairing $a$ with itself, then $\{a,b\}$, and then the pair of these two <sets>. The <axiom of extensionality> supplies the usual uniqueness of each specified <set>. In particular, no use of <Axiom schema of replacement> is needed to construct a single <ordered pair> from two given <sets>.
To recover the coordinates from $P=\langle a,b\rangle$, observe that
$$
\bigcap P=\{a\},\qquad \bigcup P=\{a,b\}.
$$
The first <equality> recovers $a$. Once $a$ is known, the second recovers $b$: if its <union> is the <singleton> $\{a\}$ then $b=a$, and otherwise $b$ is its unique element different from $a$. Hence <equality> of two encoded pairs forces <equality> of both coordinates, including the degenerate case $a=b$.
\b[The first <ordered triple> encoding works.] If
$$
\langle a,\langle b,c\rangle\rangle=\langle a',\langle b',c'\rangle\rangle,
$$
<injectivity> of the <ordered pair> construction first gives $a=a'$ and $\langle b,c\rangle=\langle b',c'\rangle$, and a second application gives $b=b'$ and $c=c'$. The construction uses only two successive <ordered pair> constructions, so is a <set> as well.
Back to article page
