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 On
Assertion oneli B A B On


Step Hyp Ref Expression
1 on.1 A On
2 onelon A On B A B On
3 1 2 mpan B A B On