Theorem df2o2

Description: Expanded value of the ordinal number 2. (Contributed by NM, 29-Jan-2004)

	Ref	Expression
Assertion	df2o2	$$⊢2_{𝑜}=\left\{\varnothing ,\left\{\varnothing \right\}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df2o3	$$⊢2_{𝑜}=\left\{\varnothing ,1_{𝑜}\right\}$$
2		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
3	2	preq2i	$$⊢\left\{\varnothing ,1_{𝑜}\right\}=\left\{\varnothing ,\left\{\varnothing \right\}\right\}$$
4	1 3	eqtri	$$⊢2_{𝑜}=\left\{\varnothing ,\left\{\varnothing \right\}\right\}$$