Metamath Proof Explorer


Theorem onsucb

Description: A class is an ordinal number if and only if its successor is an ordinal number. Biconditional form of onsuc . (Contributed by NM, 9-Sep-2003)

Ref Expression
Assertion onsucb A On suc A On

Proof

Step Hyp Ref Expression
1 ordsuc Ord A Ord suc A
2 sucexb A V suc A V
3 1 2 anbi12i Ord A A V Ord suc A suc A V
4 elon2 A On Ord A A V
5 elon2 suc A On Ord suc A suc A V
6 3 4 5 3bitr4i A On suc A On