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