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

Metamath Proof Explorer

Theorem on0eln0

Description: An ordinal number contains zero iff it is nonzero. (Contributed by NM, 6-Dec-2004)

Ref Expression
Assertion on0eln0 ⊢ A ∈ On → ∅ ∈ A ↔ A ≠ ∅

Proof

Step Hyp Ref Expression
1 eloni ⊢ A ∈ On → Ord ⁡ A
2 ord0eln0 ⊢ Ord ⁡ A → ∅ ∈ A ↔ A ≠ ∅
3 1 2 syl ⊢ A ∈ On → ∅ ∈ A ↔ A ≠ ∅