Metamath Proof Explorer


Theorem sucon

Description: The class of all ordinal numbers is its own successor. (Contributed by NM, 12-Sep-2003)

Ref Expression
Assertion sucon
|- suc On = On

Proof

Step Hyp Ref Expression
1 onprc
 |-  -. On e. _V
2 sucprc
 |-  ( -. On e. _V -> suc On = On )
3 1 2 ax-mp
 |-  suc On = On