Definition df-4o

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

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

Detailed syntax breakdown

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