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 𝐴𝐵𝐴 ) → 𝐵 ∈ On )

Proof

Step Hyp Ref Expression
1 ordelord ( ( Ord 𝐴𝐵𝐴 ) → Ord 𝐵 )
2 elong ( 𝐵𝐴 → ( 𝐵 ∈ On ↔ Ord 𝐵 ) )
3 2 adantl ( ( Ord 𝐴𝐵𝐴 ) → ( 𝐵 ∈ On ↔ Ord 𝐵 ) )
4 1 3 mpbird ( ( Ord 𝐴𝐵𝐴 ) → 𝐵 ∈ On )