===== Successor set =====
==== Set ====
| @#55CCEE: context     | @#55CCEE: $X$ |
| @#FFBB00: definiendum | @#FFBB00: $ {\mathrm{succ}}\ X \equiv X \cup \{X\} $ |

==== Discussion ====
=== Theorems ===
^ $ 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 $ ^
=== Reference ===
Wikipedia: [[http://en.wikipedia.org/wiki/Successor_ordinal|Successor ordinal]]

ProofWiki: [[http://www.proofwiki.org/wiki/Definition:Successor_Set|Successor set]]
==== Parents ====
=== Requirements ===
[[Singleton]], [[Union]]