Theorem. Show that the definition of the ordered pair $(x,y) := \{ \{ x \}, \{ x, y \} \}$ obeys the property (3.5)
$$ (x,y) = (x',y') \leftrightarrow x' = x \wedge y' = y. $$
Proof.
Two sets are equal iff every element of one set is element of the other set and vice versa:
\begin{equation}\label{eqn_idSets}
\{ \{ x \}, \{ x, y \} \} = \{ \{ x' \}, \{ x', y' \} \} \leftrightarrow
(\forall z) \: z \in \{ \{ x \}, \{ x, y \} \} \leftrightarrow z \in \{ \{ x' \}, \{ x', y' \} \}.
\end{equation}
Since $ \{ \{ x \}, \{ x, y \} \} $ is, according to the pair set axiom (3.3), a set, we also have
$$ z \in \{ \{ x \}, \{ x, y \} \} \leftrightarrow z = \{ x \} \vee z = \{ x, y \}. $$
Inserting this identity into (\ref{eqn_idSets}) yields
$$ (\forall z) \: z = \{ x \} \vee z = \{ x, y \} \leftrightarrow z = \{ x' \} \vee z = \{ x', y' \}, $$
or, equivalently,
\begin{equation}\label{eqn_expand}
(\forall z) \: (z = \{ x \} \vee z = \{ x, y \} \rightarrow z = \{ x' \} \vee z = \{ x', y' \})
\wedge (z = \{ x \} \vee z = \{ x,y \} \leftarrow z = \{ x' \} \vee z = \{ x',y' \}).
\end{equation}
If $x = y$, (\ref{eqn_idSets}) requires that
$$ (\forall z) \: z \in \{ \{ x \} \} \leftrightarrow z \in \{ \{ x' \}, \{ x', y' \} \}. $$
In this case the equivalence holds iff $x' = y'$ such that $x = x'$ and $y = y'$.
If $x \neq y$, (\ref{eqn_expand}) yields two implications for the 1st clause of the conjunction:
\begin{align}\label{eqn_impxneqy1}
z = \{ x \} & \rightarrow z = \{ x' \} \vee z = \{ x', y' \}, \\ \label{eqn_impxneqy2}
z = \{ x,y \} & \rightarrow z = \{ x' \} \vee z = \{ x', y' \}. \\
\end{align}
Since for two sets to be equal they need to have the same number of elements, ($\ref{eqn_impxneqy1}$) and ($\ref{eqn_impxneqy2}$) reduce to
\begin{align} \label{eqn_impxneqy3}
z = \{ x \} & \rightarrow z = \{ x' \}, \\ \label{eqn_impxneqy4}
z = \{ x,y \} & \rightarrow z = \{ x', y' \}. \\
\end{align}
From ($\ref{eqn_impxneqy3}$) we have that $x = x'$ while ($\ref{eqn_impxneqy4}$) requires that
$$ \{ x,y \} = \{ x', y' \} \stackrel{(\ref{eqn_impxneqy3})}{\longrightarrow} \{ x,y \} = \{ x, y' \} \rightarrow y = y'. $$
Summarizing the above yields
$$ \{ \{ x \}, \{ x, y \} \} = \{ \{ x' \}, \{ x', y' \} \} \leftrightarrow (x = x' \wedge y = y').$$
$\Box$
2015 FEB 07 (v1.0)