$$
\newcommand\liff{\leftrightarrow}
\newcommand\lif{\rightarrow}
\newcommand\lfi{\leftarrow}
\newcommand\ordp[2]{\langle #1,#2 \rangle}
\newcommand\mset[1]{\{ #1 \}}
\newcommand\isRel[1]{#1 \text{ is a relation}}
\newcommand\isFunc[1]{#1 \text{ is a function}}
\newcommand\isOneOne[1]{#1 \text{ is one-one}}
\newcommand{\fitch}[1]{\begin{array}{rlr}#1\end{array}}
\newcommand{\fcol}[1]{\begin{array}{r}#1\end{array}} %FirstColumn
\newcommand{\scol}[1]{\begin{array}{l}#1\end{array}} %SecondColumn
\newcommand{\tcol}[1]{\begin{array}{l}#1\end{array}} %ThirdColumn
\newcommand{\subcol}[1]{\begin{array}{|l}#1\end{array}} %SubProofColumn
\newcommand{\startsub}{\\[-0.29em]} %adjusts line spacing slightly
\newcommand{\endsub}{\startsub} %adjusts line spacing slightly
\newcommand{\fendl}{\\[0.044em]} %adjusts line spacing slightly
$$
$$\ordp{a}{b} = p \iff \forall Z[Z \in p \liff \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b]]$$
In this definition, $p$ is our ordered pair, and every set $Z$ in $p$ has to be either $\mset{a}$ or $\mset{a,b}$. This is more explicit with the equivalent set of definitions:
$$
\mset{a} = p \iff \forall x[x \in p \liff x = a] \\
\mset{a,b} = p \iff \forall x[x \in p \liff x = a \lor x = b] \\
\ordp{a}{b} = p \iff \forall Z [Z \in p \liff Z=\mset{a} \lor Z=\mset{a,b}] \\
$$
The former is more in line with the question, since it is a single definition and uses only primitive symbols. However, I found the latter nicer to work with, as it makes proofs a lot less verbose. In any case, they are equivalent, so a proof that is valid for one is valid for the other.
We may prove that set-theory guarantees their unique existence. The first definition will be used in this example.
The following statements trivially follow from Paring, Specification and Extensionality:
$$
\begin{array}{l}
\text{[1]}:\forall a \exists A \forall x[x \in A \liff x = a] \\
\text{[2]}:\forall a \forall b \exists A \forall x[x \in A \liff x = a \lor x = b] \\
\text{[3]}:\forall p \forall q \forall a[\forall x[x \in p \liff x = a] \land \forall x[x \in q \liff x = a] \lif p = q] \\
\text{[4]}:\forall p \forall q \forall a \forall b[\forall x[x \in p \liff x = a \lor x = b] \land \forall x[x \in q \liff x = a \lor x = b] \lif p = q] \\
\end{array}
$$
We may use the first two to introduce the sets $A_{\alpha a}$ and $A_{\beta ab}$, which represent $\mset{a}$ and $\mset{a,b}$, and then introduce $p_{\alpha ab}$, which represents our ordered pair:
$$
\small
\fitch{
\fcol{1:\fendl 2:\fendl 3:\fendl 4:\fendl 5:\fendl 6:\fendl 7:\fendl \vdots\fendl
}
& \scol {
\exists A \forall x[x \in A \liff x = a] \\
\exists A \forall x[x \in A \liff x = a \lor x = b] \\
\forall x[x \in A_{\alpha a} \liff x = a] \\
\forall x[x \in A_{\beta ab} \liff x = a \lor x = b] \\
\exists A \forall x[x \in A \liff x = A_{\alpha a} \lor x = A_{\beta ab}] \\
\forall x[x \in p_{\alpha ab} \liff x = A_{\alpha a} \lor x = A_{\beta ab}] \\
Z \in p_{\alpha ab} \liff Z = A_{\alpha a} \lor Z = A_{\beta ab} \\
\rlap{\vdots} \hphantom{\subcol{\subcol{\forall x[x \in Z \liff x=a \lor x=b] \land \forall x[x \in A_{\beta ab} \liff x=a \lor x=b] \lif Z = A_{\beta ab}}}} \\
}
& \tcol{
[1]\ \forall\text{E} \fendl
[2]\ \forall\text{E} \fendl
1\ \exists\text{E} \fendl
2\ \exists\text{E} \fendl
[2]\ \forall\text{E}[a/A_{\alpha a},b/A_{\beta ab}] \fendl
5\ \exists\text{E}[A/p_{\alpha ab}] \fendl
6\ \forall\text{E}[x/Z] \fendl
\rlap{\vdots} \hphantom{aaa\ \forall\text{E}[a/A_{\alpha a},b/A_{\beta ab}]} \fendl
}
}
$$
Then, we prove that $p_{\alpha ab}$ follows the defined properties, which means that a being with these properties exists (line $36$):
$$
\small
\fitch{
\fcol{\vdots\fendl 8:\fendl 9:\fendl 10:\fendl 11:\fendl 12:\fendl 13:\fendl 14:\fendl 15:\fendl 16:\fendl 17:\fendl 18:\fendl 19:\fendl 20:\fendl 21:\fendl 22:\fendl 23:\fendl 24:\fendl 25:\fendl 26:\fendl 27:\fendl 28:\fendl 29:\fendl 30:\fendl 31:\fendl 32:\fendl 33:\fendl 34:\fendl 35:\fendl 36:\fendl \vdots\fendl
}
& \scol {
\rlap{\vdots}
\startsub\subcol{
Z \in p_{\alpha ab} \\
\hline
Z = A_{\alpha a} \lor Z = A_{\beta ab}
\startsub\subcol{
Z = A_{\alpha a} \\
\hline
\forall x[x \in Z \liff x = a] \\
\forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b] \\
}\endsub
Z = A_{\alpha a} \lif \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b]
\startsub\subcol{
Z = A_{\beta ab} \\
\hline
\forall x[x \in Z \liff x = a \lor x = b] \\
\forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b] \\
}\endsub
Z = A_{\beta ab} \lif \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b] \\
\forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b] \\
}\endsub
Z \in p_{\alpha ab} \lif \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b]
\startsub\subcol{
\forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b]
\startsub\hline\subcol{
\forall x[x \in Z \liff x = a] \\
\hline
\forall x[x \in Z \liff x=a] \land \forall x[x \in A_{\alpha a} \liff x=a] \lif Z = A_{\alpha a} \\
Z = A_{\alpha a} \\
Z = A_{\alpha a} \lor Z = A_{\beta ab} \\
}\endsub
\forall x[x \in Z \liff x = a] \lif Z = A_{\alpha a} \lor Z = A_{\beta ab}
\startsub\subcol{
\forall x[x \in Z \liff x = a \lor x = b] \\
\hline
\forall x[x \in Z \liff x=a \lor x=b] \land \forall x[x \in A_{\beta ab} \liff x=a \lor x=b] \lif Z = A_{\beta ab} \\
Z = A_{\beta ab} \\
Z = A_{\alpha a} \lor Z = A_{\beta ab} \\
}\endsub
\forall x[x \in Z \liff x = a \lor x = b] \lif Z = A_{\alpha a} \lor Z = A_{\beta ab} \\
Z = A_{\alpha a} \lor Z = A_{\beta ab} \\
Z \in p_{\alpha ab}
}\endsub
\forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b] \lif Z \in p_{\alpha ab} \\
Z \in p_{\alpha ab} \liff \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b] \\
\forall Z[Z \in p_{\alpha ab} \liff \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b]] \\
\exists p \forall Z[Z \in p \liff \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b]] \\
\rlap{\vdots} \\
}
& \tcol{
\rlap{\vdots} \hphantom{aaa\ \forall\text{E}[a/A_{\alpha a},b/A_{\beta ab}]} \fendl
\text{P}[Z] \fendl
7,8\ {\liff}\text{E} \fendl
\text{P}[Z] \fendl
3,10\ {=}\text{S}[A_{\alpha a}/Z] \fendl
11\ {\lor}\text{I} \fendl
10,12\ {\lif}\text{I}\ \fendl
\text{P}[Z] \fendl
4,14\ {=}\text{S}[A_{\beta ab}/Z] \fendl
15\ {\lor}\text{I} \fendl
14,16\ {\lif}\text{I} \fendl
9,13,17\ {\lor}\text{E} \fendl
8,18\ {\lif}\text{I} \fendl
\text{P}[Z,a,b] \fendl
\text{P}[Z,a,b] \fendl
[3]\ \forall\text{E}[p/Z,q/A_{\alpha a}] \fendl
3,21,22\ {\lif}\text{E} \fendl
22\ {\lor}\text{I} \fendl
20,23\ {\lif}\text{I} \fendl
\text{P}[Z,a,b] \fendl
[4]\ \forall\text{E}[p/Z,q/A_{\beta ab}] \fendl
4,26,27\ {\lif}\text{E} \fendl
27\ {\lor}\text{I} \fendl
25,28\ {\lif}\text{I} \fendl
20,25,30\ {\lor}\text{E} \fendl
7,31\ {\liff}\text{E} \fendl
20,32\ {\lif}\text{I} \fendl
19,33\ {\liff}\text{I} \fendl
34\ \forall\text{I}\ \fendl
35\ \exists\text{I}\ \fendl
\rlap{\vdots} \hphantom{aaa\ \forall\text{E}[a/A_{\alpha a},b/A_{\beta ab}]} \fendl
}
}$$
Then we prove that this being is unique, by showing that if any two sets $p$ and $q$ follow these properties, they are one and the same (line $45$):
$$
\small
\fitch{
\fcol{\vdots\fendl 37:\fendl 38:\fendl 39:\fendl 40:\fendl 41:\fendl 42:\fendl 43:\fendl 44:\fendl\fendl\fendl 45:\fendl\fendl\fendl 46:\fendl
}
& \scol {
\rlap{\vdots} \hphantom{\subcol{\subcol{\forall x[x \in Z \liff x=a \lor x=b] \land \forall x[x \in A_{\beta ab} \liff x=a \lor x=b] \lif Z = A_{\beta ab}}}}
\startsub\subcol{
\forall Z[Z \in p \liff \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b]] \\
\forall Z[Z \in q \liff \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b]] \\
\hline
Z \in p \liff \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b] \\
Z \in q \liff \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b] \\
Z \in p \liff Z \in q \\
\forall Z[Z \in p \liff Z \in q] \\
p = q \\
} \endsub
\forall Z[Z \in p \liff \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b]] \\\quad\ \land \forall Z[Z \in q \liff \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b]] \\\quad \lif p = q \\
\forall p \forall q[\forall Z[Z \in p \liff \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b]] \\\quad\ \land \forall Z[Z \in q \liff \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b]] \\\quad \lif p = q] \\
\exists p! \forall Z[Z \in p \liff \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b]] \\
}
& \tcol{
\rlap{\vdots} \hphantom{aaa\ \forall\text{E}[a/A_{\alpha a},b/A_{\beta ab}]} \\
\text{P}[p,a,b] \fendl
\text{P}[q,p,a,b] \fendl
37\ \forall\text{E} \fendl
38\ \forall\text{E} \fendl
39,40\ {\liff}\text{Tr} \fendl
41\ \forall\text{I} \fendl
42,\text{Ext.}\ \forall\text{I} \fendl
37,38,43\ {\lif}\text{I} \fendl\fendl\fendl
45\ \forall\text{I} \fendl\fendl\fendl
36,45\ \exists!\text{I} \fendl
}
}
$$
As such, there exists a unique $p$ with these properties (line $46$).
We may also prove that they obey the characteristeric property for ordered pairs, namely: $\forall x \forall y \forall a \forall b[\ordp{x}{y} = \ordp{a}{b} \liff x = a \land y = b]$. The second definition will be used in this example.
The following statements trivially follow from the definitions of $\mset{a}$ and $\mset{a,b}$, and Extentionality:
$$
\begin{array}{l}
\text{[1]}:\forall a \forall b [\mset{a} = \mset{b} \liff a=b] \\
\text{[2]}:\forall a [\mset{a,a} = \mset{a}] \\
\text{[3]}:\forall a \forall b [\mset{a,b} = \mset{a} \liff a=b] \\
\text{[4]}:\forall a \forall b \forall c [a \neq b \lif \mset{c} \neq \mset{a,b}] \\
\text{[5]}:\forall a \forall b \forall c [\mset{a,b} = \mset{a,c} \liff b = c] \\
\end{array}
$$
We start by proving the trivial implication from RHS to LHS:
$$
\small
\fitch{
\fcol{
1:\fendl 2:\fendl 3:\fendl 4:\fendl \vdots\fendl
}
& \scol {
\subcol{
x=a \land y=b \\
\hline
\ordp{x}{y} = \ordp{x}{y} \\
\ordp{x}{y} = \ordp{a}{b} \\
} \endsub
x=a \land y=b \lif \ordp{x}{y} = \ordp{a}{b} \\
\rlap{\vdots} \hphantom{\subcol{\mset{x,y}=\mset{a} \lor \mset{x,y}=\mset{a,b} \liff \mset{x,y}=\mset{x} \lor \mset{x,y}=\mset{x,y}}} \\
}
& \tcol{
\text{P}[x,y,a,b] \fendl
\text{T} \fendl
1,2\ {=}\text{S} \fendl
1,3\ {\lif}\text{I} \fendl
\rlap{\vdots}\hphantom{\text{Def.}\ \forall\text{E}[a/x,b/y,p/\ordp{a}{b}]} \fendl
}
}
$$
For the trickier LHS to RHS, we start by assuming that $\ordp{x}{y} = \ordp{a}{b}$ and using the definition to establish a relationship between the sets (line $14$). From that relationship, we extract some useful statements about them (lines $19$ to $22$):
$$
\small
\fitch{
\fcol{
\vdots\fendl 5:\fendl 6:\fendl 7:\fendl 8:\fendl 9:\fendl 10:\fendl 11:\fendl 12:\fendl 13:\fendl 14:\fendl 15:\fendl 16:\fendl 17:\fendl 18:\fendl 19:\fendl 20:\fendl 21:\fendl 22:\fendl \vdots\fendl
}
& \scol {
\subcol{
\rlap{\vdots} \\
\ordp{x}{y} = \ordp{a}{b} \\
\hline
\ordp{a}{b} = \ordp{x}{y} \liff \forall Z [Z \in \ordp{x}{y} \liff Z=\mset{a} \lor Z=\mset{a,b}] \\
\ordp{x}{y} = \ordp{a}{b} \liff \forall Z [Z \in \ordp{a}{b} \liff Z=\mset{x} \lor Z=\mset{x,y}] \\
\forall Z [Z \in \ordp{x}{y} \liff Z=\mset{x} \lor Z=\mset{x,y}] \\
\forall Z [Z \in \ordp{a}{b} \liff Z=\mset{a} \lor Z=\mset{a,b}] \\
Z \in \ordp{x}{y} \liff Z=\mset{a} \lor Z=\mset{a,b} \\
Z \in \ordp{a}{b} \liff Z=\mset{x} \lor Z=\mset{x,y} \\
Z \in \ordp{a}{b} \liff Z=\mset{a} \lor Z=\mset{a,b} \\
Z=\mset{a} \lor Z=\mset{a,b} \liff Z=\mset{x} \lor Z=\mset{x,y} \\
\forall Z [Z=\mset{a} \lor Z=\mset{a,b} \liff Z=\mset{x} \lor Z=\mset{x,y}] \\
\mset{a}=\mset{a} \lor \mset{a}=\mset{a,b} \liff \mset{a}=\mset{x} \lor \mset{a}=\mset{x,y} \\
\mset{x}=\mset{a} \lor \mset{x}=\mset{a,b} \liff \mset{x}=\mset{x} \lor \mset{x}=\mset{x,y} \\
\mset{a,b}=\mset{a} \lor \mset{a,b}=\mset{a,b} \liff \mset{a,b}=\mset{x} \lor \mset{a,b}=\mset{x,y} \\
\mset{x,y}=\mset{a} \lor \mset{x,y}=\mset{a,b} \liff \mset{x,y}=\mset{x} \lor \mset{x,y}=\mset{x,y} \\
\mset{a}=\mset{x} \lor \mset{a}=\mset{x,y} \\
\mset{x}=\mset{a} \lor \mset{x}=\mset{a,b} \\
\mset{a,b}=\mset{x} \lor \mset{a,b}=\mset{x,y} \\
\mset{x,y}=\mset{a} \lor \mset{x,y}=\mset{a,b} \\
\rlap{\vdots}
}
}
& \tcol{
\rlap{\vdots}\hphantom{\text{Def.}\ \forall\text{E}[a/x,b/y,p/\ordp{a}{b}]} \fendl
\text{P}[x,y,a,b] \fendl
\text{Def.}\ \forall\text{E}[p/\ordp{x}{y}] \fendl
\text{Def.}\ \forall\text{E}[a/x,b/y,p/\ordp{a}{b}] \fendl
5,6\ {\liff}\text{E} \fendl
5,7\ {\liff}\text{E} \fendl
8\ \forall\text{E} \fendl
9\ \forall\text{E} \fendl
5,10\ {=}\text{S} \fendl
11,12\ {\liff}\text{Tr} \fendl
13\ \forall\text{I} \fendl
14\ \forall\text{E}[Z/\mset{a}] \fendl
14\ \forall\text{E}[Z/\mset{x}] \fendl
14\ \forall\text{E}[Z/\mset{a,b}] \fendl
14\ \forall\text{E}[Z/\mset{x,y}] \fendl
15\ {\liff}\text{E} \fendl
16\ {\liff}\text{E} \fendl
17\ {\liff}\text{E} \fendl
18\ {\liff}\text{E} \fendl
\rlap{\vdots}\hphantom{\text{Def.}\ \forall\text{E}[a/x,b/y,p/\ordp{a}{b}]} \fendl
}
}
$$
Now, either $a = b$ or $a \neq b$. So we may prove that in both cases it follows that $a=x$ and $b=y$. In the case that $a = b$:
$$
\small
\fitch{
\fcol{
\vdots\fendl 23:\fendl 24:\fendl 25:\fendl 26:\fendl 27:\fendl 28:\fendl 29:\fendl 30:\fendl 31:\fendl 32:\fendl 33:\fendl 34:\fendl 35:\fendl 36:\fendl 37:\fendl 38:\fendl 39:\fendl 40:\fendl 41:\fendl \vdots\fendl
}
& \scol {
\subcol{
\rlap{\vdots} \hphantom{\mset{x,y}=\mset{a} \lor \mset{x,y}=\mset{a,b} \liff \mset{x,y}=\mset{x} \lor \mset{x,y}=\mset{x,y}} \\
a=b \lor a \neq b
\startsub\subcol{
a = b \\
\hline
\mset{x}=\mset{a} \lor \mset{x}=\mset{a,b} \\
\mset{x}=\mset{a} \lor \mset{x}=\mset{a,a} \\
\mset{a,a} = \mset{a} \\
\mset{x}=\mset{a} \lor \mset{x}=\mset{a} \\
\mset{x}=\mset{a} \\
\mset{x}=\mset{a} \liff x=a \\
x=a \\
\mset{x,y}=\mset{a} \lor \mset{x,y}=\mset{a,b} \\
x=b \\
\mset{x,y}=\mset{x} \lor \mset{x,y}=\mset{x,x} \\
\mset{x,x}=\mset{x} \\
\mset{x,y}=\mset{x} \lor \mset{x,y}=\mset{x} \\
\mset{x,y}=\mset{x} \\
\mset{x,y}=\mset{x} \liff x=y \\
x=y \\
y=b \\
} \endsub
a=b \lif (x=a \land y=b) \\
\rlap{\vdots} \hphantom{\mset{x,y}=\mset{a} \lor \mset{x,y}=\mset{a,b} \liff \mset{x,y}=\mset{x} \lor \mset{x,y}=\mset{x,y}} \\
}
}
& \tcol{
\rlap{\vdots}\hphantom{\text{Def.}\ \forall\text{E}[a/x,b/y,p/\ordp{a}{b}]} \fendl
\text{T} \fendl
\text{P}[x,y,a,b] \fendl
20\ \text{C} \fendl
24,25\ {=}\text{S}[b/a] \fendl
[2]\ \forall\text{E} \fendl
27,26\ {=}\text{S}[\mset{a,a}/\mset{a}] \fendl
28\ {\lor}\text{E} \fendl
[1]\ \forall\text{E}[a/x,b/a] \fendl
29,30\ {\liff}\text{E} \fendl
22\ \text{C}\ \fendl
24,31\ {=}\text{Tr} \fendl
32,33\ {=}\text{S}[b/x] \fendl
[2]\ \forall\text{E}[a/x] \fendl
34,35\ {=}\text{S}[\mset{x,x}/\mset{x}] \fendl
36\ {\lor}\text{E} \fendl
[3]\ \forall\text{E}[a/x,b/y] \fendl
37,38\ {\liff}\text{E} \fendl
33,39\ {=}\text{Tr} \fendl
24,31,40\ {\lif}\text{I} \fendl
\rlap{\vdots}\hphantom{\text{Def.}\ \forall\text{E}[a/x,b/y,p/\ordp{a}{b}]} \fendl
}
}
$$
In the case that $a \neq b$:
$$
\small
\fitch{
\fcol{\vdots\fendl 42:\fendl 43:\fendl 44:\fendl 45:\fendl 46:\fendl 47:\fendl 48:\fendl 49:\fendl 50:\fendl 51:\fendl 52:\fendl 53:\fendl 54:\fendl 55:\fendl 56:\fendl 57:\fendl 58:\fendl
}
& \scol {
\subcol{
\rlap{\vdots} \hphantom{\mset{x,y}=\mset{a} \lor \mset{x,y}=\mset{a,b} \liff \mset{x,y}=\mset{x} \lor \mset{x,y}=\mset{x,y}}
\startsub\subcol{
a \neq b \\
\hline
\mset{x}=\mset{a} \lor \mset{x}=\mset{a,b} \\
a \neq b \lif \mset{x} \neq \mset{a,b}\\
\mset{x} \neq \mset{a,b} \\
\mset{x}=\mset{a} \\
\mset{x}=\mset{a} \liff x=a \\
x = a \\
\mset{a,b}=\mset{x} \lor \mset{a,b}=\mset{x,y} \\
\mset{a,b}=\mset{x,y} \\
\mset{a,b}=\mset{a,y} \\
\mset{a,b}=\mset{a,y} \liff b=y\\
b = y
} \endsub
a \neq b \lif (x=a \land y=b) \\
x=a \land y=b
} \endsub
\ordp{x}{y} = \ordp{a}{b} \lif x=a \land y=b \\
\ordp{x}{y} = \ordp{a}{b} \liff x=a \land y=b \\
\forall x \forall y \forall a \forall b[\ordp{x}{y} = \ordp{a}{b} \liff x=a \land y=b] \\
}
& \tcol{
\rlap{\vdots}\hphantom{\text{Def.}\ \forall\text{E}[a/x,b/y,p/\ordp{a}{b}]} \fendl
\text{P}[x,y,a,b] \fendl
20\ \text{C} \fendl
[4]\ \forall\text{E}[c/x] \fendl
42,44\ {\lif}\text{E} \fendl
43,45\ {\lor}\text{E} \fendl
[1]\ \forall\text{E}[a/x,b/a] \fendl
46,47\ {\liff}\text{E} \fendl
21\ \text{C} \fendl
45,49\ {\lor}\text{E} \fendl
48,50\ {=}\text{S}[x/a] \fendl
[5]\ \forall\text{E}[c/y] \fendl
51,52\ {\liff}\text{E} \fendl
42,53\ {\lif}\text{I} \fendl
23,41,54\ \text{TI} \fendl
5,55\ {\lif}\text{I} \fendl
4,56\ {\liff}\text{I}\ \fendl
57\ \forall\text{I}\ \fendl
}
}
$$
As such, the definitions obey the characteristic property for ordered pairs.