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 e. On <-> suc A e. On )

Proof

Step Hyp Ref Expression
1 ordsuc
 |-  ( Ord A <-> Ord suc A )
2 sucexb
 |-  ( A e. _V <-> suc A e. _V )
3 1 2 anbi12i
 |-  ( ( Ord A /\ A e. _V ) <-> ( Ord suc A /\ suc A e. _V ) )
4 elon2
 |-  ( A e. On <-> ( Ord A /\ A e. _V ) )
5 elon2
 |-  ( suc A e. On <-> ( Ord suc A /\ suc A e. _V ) )
6 3 4 5 3bitr4i
 |-  ( A e. On <-> suc A e. On )