Definition df-1o

Description: Define the ordinal number 1. Definition 2.1 of Schloeder p. 4. (Contributed by NM, 29-Oct-1995)

	Ref	Expression
Assertion	df-1o	⊢ 1o = suc ∅

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c1o	⊢ 1o
1		c0	⊢ ∅
2	1	csuc	⊢ suc ∅
3	0 2	wceq	⊢ 1o = suc ∅