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

Metamath Proof Explorer

Theorem 1n0

Description: Ordinal one is not equal to ordinal zero. (Contributed by NM, 26-Dec-2004)

Ref Expression
Assertion 1n0 1o ≠ ∅

Proof

Step Hyp Ref Expression
1 df1o2 ⊢ 1o = { ∅ }
2 0ex ⊢ ∅ ∈ V
3 2 snnz ⊢ { ∅ } ≠ ∅
4 1 3 eqnetri ⊢ 1o ≠ ∅