Metamath Proof Explorer

Theorem oneli

Description: A member of an ordinal number is an ordinal number. Theorem 7M(a) of Enderton p. 192. (Contributed by NM, 11-Jun-1994)

Ref Expression
Hypothesis on.1 
|- A e. On
Assertion oneli 
|- ( B e. A -> B e. On )

Proof

Step Hyp Ref Expression
1 on.1 
 |-  A e. On
2 onelon 
 |-  ( ( A e. On /\ B e. A ) -> B e. On )
3 1 2 mpan 
 |-  ( B e. A -> B e. On )