Metamath Proof Explorer


Theorem ordelon

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

Ref Expression
Assertion ordelon Ord A B A B On

Proof

Step Hyp Ref Expression
1 ordelord Ord A B A Ord B
2 elong B A B On Ord B
3 2 adantl Ord A B A B On Ord B
4 1 3 mpbird Ord A B A B On