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	$$⊢1_{𝑜}\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-1o	$$⊢1_{𝑜}=\mathrm{suc}\varnothing$$
2		nsuceq0	$$⊢\mathrm{suc}\varnothing \ne \varnothing$$
3	1 2	eqnetri	$$⊢1_{𝑜}\ne \varnothing$$