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

In the setting of Class Theory NBG: the Axioms, Standing Conventions and Basic Notation, formulas may be written with abbreviations, and predicative is then meant as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (vi); set variables and class variables are as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (i), and sets and classes are assigned to them as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (iv).

Throughout, $s$ is a variable of either kind, $t'_{1}$ and $t'_{2}$ are distinct set variables other than $s$, and $\pi_{1}$, $\pi_{2}$ and $\pi_{3}$ are the formulas obtained, as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (vi), by eliminating the unordered pair, the singleton and the successor, used as defined set symbols, from $s=\{t'_{1},t'_{2}\}$, $s=\{t'_{1}\}$ and $s=S(t'_{1})$. For variables $t_{1}$ and $t_{2}$ of either kind, not necessarily distinct and possibly equal to $s$, the formulas $s=\{t_{1},t_{2}\}$, $s=\{t_{1}\}$ and $s=S(t_{1})$ are $\pi_{1}[t/t']$, $\pi_{2}[t/t']$ and $\pi_{3}[t/t']$, formed as in 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) with $t'_{i}$ for $v_{i}$ and $t_{i}$ for $y_{i}$ ($k=2$, $1$ and $1$ respectively).

(i) The formula $s=\{t_{1},t_{2}\}$ is predicative; and when sets are assigned to $t_{1}$ and $t_{2}$, it holds if and only if the value of $s$ is the unordered pair of the values of $t_{1}$ and $t_{2}$.

(ii) The formula $s=\{t_{1}\}$ is predicative; and when a set is assigned to $t_{1}$, it holds if and only if the value of $s$ is the singleton of the value of $t_{1}$.

(iii) The formula $s=S(t_{1})$ is predicative; and when a set is assigned to $t_{1}$, it holds if and only if the value of $s$ is the successor of the value of $t_{1}$.