Theorem 1n0

Description: Ordinal one is not equal to ordinal zero. (Contributed by NM, 26-Dec-2004) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026)

	Ref	Expression
Assertion	1n0	⊢ 1o ≠ ∅

Proof

Step	Hyp	Ref	Expression
1		df-1o	⊢ 1o = suc ∅
2		nsuceq0	⊢ suc ∅ ≠ ∅
3	1 2	eqnetri	⊢ 1o ≠ ∅