Proof of Atomic Predicative Formulas: Equality with Unordered Pairs, Singletons and Successors

Let $x$, $y$, $z$ and $w$ be set variables. Let $\theta_{1}(z,x,y)$, $\theta_{2}(z,x)$ and $\theta_{3}(z,x)$ be the formulas

$$\forall w\,(w\in z\Leftrightarrow(w=x\vee w=y)),\qquad \forall w\,(w\in z\Leftrightarrow w=x),\qquad \forall w\,(w\in z\Leftrightarrow(w\in x\vee w=x)).$$

By Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (iv) and The Successor of a Set (i), these are the conditions by which the unordered pair, the singleton and the successor are introduced as defined set symbols, so that for all sets $x$, $y$ and $z$,

$$\theta_{1}(z,x,y)\iff z=\{x,y\},\qquad \theta_{2}(z,x)\iff z=\{x\},\qquad \theta_{3}(z,x)\iff z=S(x).$$

The formulas before renaming. By the elimination rule of Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (viii), applied to the atomic formulas $s=\{t'_{1},t'_{2}\}$, $s=\{t'_{1}\}$ and $s=S(t'_{1})$,

$$\pi_{1}=\exists z\,(\theta_{1}(z,t'_{1},t'_{2})\wedge s=z),\qquad \pi_{2}=\exists z\,(\theta_{2}(z,t'_{1})\wedge s=z),\qquad \pi_{3}=\exists z\,(\theta_{3}(z,t'_{1})\wedge s=z),$$

with $z$ a set variable occurring nowhere else. The three expressions apply quantifiers only to the set variables $z$ and $w$, none to a class variable, so $\pi_{1}$, $\pi_{2}$ and $\pi_{3}$ are predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i).

Assign sets $u$ and $v$ to $t'_{1}$ and $t'_{2}$ and a class $A$ to $s$. Then $\pi_{1}$ holds if and only if there is a set $z$ with $z=\{u,v\}$ and $A=z$. Since $\{u,v\}$ is a set by The Empty Set, the Unordered Pair and the Singleton (ii), this holds if and only if $A=\{u,v\}$: if $A=\{u,v\}$, take $z=\{u,v\}$; conversely $A=z=\{u,v\}$. In the same way, since $\{u\}$ is a set by The Empty Set, the Unordered Pair and the Singleton (iii) and $S(u)$ is a set by The Successor of a Set (i), $\pi_{2}$ holds if and only if $A=\{u\}$, and $\pi_{3}$ holds if and only if $A=S(u)$. In particular, since $\{u,v\}$, $\{u\}$ and $S(u)$ are sets, no proper class equals them, and all three formulas fail when $A$ is a proper class.

Renaming. The free variables of $\pi_{1}$ are among $s$, $t'_{1}$ and $t'_{2}$, and those of $\pi_{2}$ and $\pi_{3}$ among $s$ and $t'_{1}$. Apply Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (i) to $\pi_{j}$ with $v_{i}=t'_{i}$ and $y_{i}=t_{i}$ ($k=2$ for $j=1$, and $k=1$ for $j=2,3$), $s$ being a further free variable, possibly among the $t_{i}$. It gives that $\pi_{j}[t/t']$ is predicative, and that, when sets are assigned to $t_{1}$ (and $t_{2}$), $\pi_{j}[t/t']$ holds if and only if $\pi_{j}$ holds with each $t'_{i}$ assigned the value of $t_{i}$ and $s$ keeping its value; when $s$ is one of the $t_{i}$, its value is that of $t_{i}$. By the previous paragraph, with $u$ and $v$ the values of $t_{1}$ and $t_{2}$ and $A$ the value of $s$, this holds if and only if the value of $s$ is $\{u,v\}$, $\{u\}$ or $S(u)$ respectively. This proves (i), (ii) and (iii).