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	$$⊢2_{𝑜}=\mathrm{suc}{1}_{𝑜}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c2o	$$class{2}_{𝑜}$$
1		c1o	$$class{1}_{𝑜}$$
2	1	csuc	$$class\mathrm{suc}{1}_{𝑜}$$
3	0 2	wceq	$$wff{2}_{𝑜}=\mathrm{suc}{1}_{𝑜}$$