Theorem df1o2

Description: Expanded value of the ordinal number 1. Definition 2.1 of Schloeder p. 4. (Contributed by NM, 4-Nov-2002)

	Ref	Expression
Assertion	df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-1o	$$⊢1_{𝑜}=\mathrm{suc}\varnothing$$
2		suc0	$$⊢\mathrm{suc}\varnothing =\left\{\varnothing \right\}$$
3	1 2	eqtri	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$