| context | $X$ |
| definiendum | $ {\mathrm{succ}}\ X \equiv X \cup \{X\} $ |
| $ X\in {\mathrm{succ}}\ X $ |
|---|
| $ ({\mathrm{succ}}\ X={\mathrm{succ}}\ Y)\Rightarrow (X=Y) $ |
| $ (Y\in {\mathrm{succ}}\ X)\Leftrightarrow (Y=X\lor Y=\{X\}) $ |
| $ X\neq {\mathrm{succ}}\ X $ |
Wikipedia: Successor ordinal
ProofWiki: Successor set