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 ∈ V
2 sucprc ( ¬ On ∈ V → suc On = On )
3 1 2 ax-mp suc On = On