Metamath Proof Explorer

Theorem ordelon

Description: An element of an ordinal class is an ordinal number. (Contributed by NM, 26-Oct-2003)

Ref Expression
Assertion ordelon 
|- ( ( Ord A /\ B e. A ) -> B e. On )

Proof

Step Hyp Ref Expression
1 ordelord 
 |-  ( ( Ord A /\ B e. A ) -> Ord B )
2 elong 
 |-  ( B e. A -> ( B e. On <-> Ord B ) )
3 2 adantl 
 |-  ( ( Ord A /\ B e. A ) -> ( B e. On <-> Ord B ) )
4 1 3 mpbird 
 |-  ( ( Ord A /\ B e. A ) -> B e. On )