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

Metamath Proof Explorer

Theorem elon2

Description: An ordinal number is an ordinal set. Part of Definition 1.2 of Schloeder p. 1. (Contributed by NM, 8-Feb-2004)

Ref Expression
Assertion elon2 ⊢ A ∈ On ↔ Ord ⁡ A ∧ A ∈ V

Proof

Step Hyp Ref Expression
1 elex ⊢ A ∈ On → A ∈ V
2 elong ⊢ A ∈ V → A ∈ On ↔ Ord ⁡ A
3 1 2 biadanii ⊢ A ∈ On ↔ A ∈ V ∧ Ord ⁡ A
4 3 biancomi ⊢ A ∈ On ↔ Ord ⁡ A ∧ A ∈ V