This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eloni

Description: An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994)

Ref Expression
Assertion eloni ( 𝐴 ∈ On → Ord 𝐴 )

Proof

Step Hyp Ref Expression
1 elong ⊢ ( 𝐴 ∈ On → ( 𝐴 ∈ On ↔ Ord 𝐴 ) )
2 1 ibi ⊢ ( 𝐴 ∈ On → Ord 𝐴 )