Theorem df2o2

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

	Ref	Expression
Assertion	df2o2	⊢ 2o = { ∅ , { ∅ } }

Proof

Step	Hyp	Ref	Expression
1		df2o3	⊢ 2o = { ∅ , 1o }
2		df1o2	⊢ 1o = { ∅ }
3	2	preq2i	⊢ { ∅ , 1o } = { ∅ , { ∅ } }
4	1 3	eqtri	⊢ 2o = { ∅ , { ∅ } }