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 (/)