Proof of The Characteristic Property of Ordered Pairs and Nested Tuples of Sets

Throughout, equal classes have the same elements, since by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §symbols the symbol $=$ is the equality of the underlying logic, so equals may be substituted for one another (substitutivity of equality).

Preliminaries. For sets $a$ and $b$, the unordered pair $\{a,b\}$ is the set given by Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique §pair: for every set $w$, $w\in\{a,b\}$ if and only if $w=a$ or $w=b$. Since every element of a class is a set by Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique §elements, the elements of $\{a,b\}$ are exactly $a$ and $b$. By The Empty Set, the Unordered Pair and the Singleton §singleton, $\{a\}=\{a,a\}$, so the only element of $\{a\}$ is $a$. By The Ordered Pair of Two Sets and Nested Tuples §pair, $(a,b)=\{\{a\},\{a,b\}\}$, so the elements of $(a,b)$ are exactly $\{a\}$ and $\{a,b\}$. We also use the following fact (P): for sets $a,b,c$, if $\{a\}=\{b,c\}$ then $b=a$ and $c=a$. Indeed $b\in\{b,c\}=\{a\}$, so $b=a$, and likewise $c\in\{b,c\}=\{a\}$ gives $c=a$.

Clause characteristic. Let $x,y,u,v$ be sets. If $x=u$ and $y=v$ then $(x,y)=(u,v)$ by substitutivity of equality (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §symbols). Conversely, suppose $(x,y)=(u,v)$. Both $\{u\}$ and $\{u,v\}$ are elements of $(u,v)=(x,y)$.

Case $x=y$. Then $\{x,y\}=\{x,x\}=\{x\}$, so the only element of $(x,y)=\{\{x\},\{x\}\}$ is $\{x\}$. Hence $\{u\}=\{x\}$ and $\{u,v\}=\{x\}$. Since $\{u\}=\{u,u\}$, fact (P) applied to $\{x\}=\{u,u\}$ gives $u=x$, and applied to $\{x\}=\{u,v\}$ gives $v=x=y$.

Case $x\ne y$. Since $\{x\}\in(u,v)$, either $\{x\}=\{u\}$ or $\{x\}=\{u,v\}$. In either case $u$ is an element of $\{x\}$ (as $u\in\{u\}$ and $u\in\{u,v\}$), so $u=x$. Since $\{x,y\}\in(u,v)$, either $\{x,y\}=\{u\}$ or $\{x,y\}=\{u,v\}$. If $\{x,y\}=\{u\}$, fact (P) gives $x=u$ and $y=u$, so $x=y$, a contradiction. Hence $\{x,y\}=\{u,v\}$, so $y\in\{u,v\}$, that is, $y=u$ or $y=v$. If $y=u$ then $y=x$, a contradiction; therefore $y=v$.

In both cases $x=u$ and $y=v$.

Clause tuples. By induction on the metatheoretic number $n\ge1$, using the recursion of The Ordered Pair of Two Sets and Nested Tuples §tuple. For $n=1$, $\langle x_{1}\rangle=x_{1}$ and $\langle y_{1}\rangle=y_{1}$, so the claim reads $x_{1}=y_{1}$ if and only if $x_{1}=y_{1}$. Suppose the claim holds for $n$, and let $x_{1},\dots,x_{n+1},y_{1},\dots,y_{n+1}$ be sets. By The Ordered Pair of Two Sets and Nested Tuples §tuple, $\langle x_{1},\dots,x_{n+1}\rangle=(\langle x_{1},\dots,x_{n}\rangle,x_{n+1})$ and $\langle y_{1},\dots,y_{n+1}\rangle=(\langle y_{1},\dots,y_{n}\rangle,y_{n+1})$, where $\langle x_{1},\dots,x_{n}\rangle$ and $\langle y_{1},\dots,y_{n}\rangle$ are sets. By the clause characteristic above, these two ordered pairs are equal if and only if $\langle x_{1},\dots,x_{n}\rangle=\langle y_{1},\dots,y_{n}\rangle$ and $x_{n+1}=y_{n+1}$, and by the induction hypothesis this holds if and only if $x_{i}=y_{i}$ for every $i$ with $1\le i\le n+1$.