Definition df-2o

Description: Define the ordinal number 2. Lemma 3.17 of Schloeder p. 10. (Contributed by NM, 18-Feb-2004)

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

Detailed syntax breakdown

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