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

Metamath Proof Explorer

Theorem onordi

Description: An ordinal number is an ordinal class. (Contributed by NM, 11-Jun-1994)

Ref Expression
Hypothesis on.1 ⊢ 𝐴 ∈ On
Assertion onordi Ord 𝐴

Proof

Step Hyp Ref Expression
1 on.1 ⊢ 𝐴 ∈ On
2 eloni ⊢ ( 𝐴 ∈ On → Ord 𝐴 )
3 1 2 ax-mp ⊢ Ord 𝐴