Definition df-3o

Description: Define the ordinal number 3. (Contributed by Mario Carneiro, 14-Jul-2013)

	Ref	Expression
Assertion	df-3o	$$⊢3_{𝑜}=\mathrm{suc}{2}_{𝑜}$$

Detailed syntax breakdown

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