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	⊢ 1o = { ∅ }

Proof

Step	Hyp	Ref	Expression
1		df-1o	⊢ 1o = suc ∅
2		suc0	⊢ suc ∅ = { ∅ }
3	1 2	eqtri	⊢ 1o = { ∅ }