Metamath Proof Explorer

Theorem elon

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

Ref Expression
Hypothesis elon.1 ⊢ A ∈ V
Assertion elon ⊢ A ∈ On ↔ Ord ⁡ A

Proof

Step Hyp Ref Expression
1 elon.1 ⊢ A ∈ V
2 elong ⊢ A ∈ V → A ∈ On ↔ Ord ⁡ A
3 1 2 ax-mp ⊢ A ∈ On ↔ Ord ⁡ A