Metamath Proof Explorer

Theorem onelon

Description: An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of BellMachover p. 469. Lemma 1.3 of Schloeder p. 1. (Contributed by NM, 26-Oct-2003)

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

Proof

Step Hyp Ref Expression
1 eloni 
 |-  ( A e. On -> Ord A )
2 ordelon 
 |-  ( ( Ord A /\ B e. A ) -> B e. On )
3 1 2 sylan 
 |-  ( ( A e. On /\ B e. A ) -> B e. On )