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 ≠ ∅