Theorem 2on0

Description: Ordinal two is not zero. (Contributed by Scott Fenton, 17-Jun-2011)

	Ref	Expression
Assertion	2on0	$$⊢2_{𝑜}\ne \varnothing$$

Proof

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