The Characteristic Property of Ordered Pairs and Nested Tuples of Sets

¶ For sets $x,y,u,v$, the ordered pairs satisfy $(x,y)=(u,v)$ if and only if $x=u$ and $y=v$.

¶ This clause is a theorem scheme of the metatheory, one theorem for each number of entries, proved by induction on that number in the metatheory. For a metatheoretic number $n\ge1$ and sets $x_{1},\dots,x_{n},y_{1},\dots,y_{n}$, the tuples satisfy $\langle x_{1},\dots,x_{n}\rangle=\langle y_{1},\dots,y_{n}\rangle$ if and only if $x_{i}=y_{i}$ for every $i$ with $1\le i\le n$.