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