Definition df-4o

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

	Ref	Expression
Assertion	df-4o	⊢ 4o = suc 3o

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c4o	⊢ 4o
1		c3o	⊢ 3o
2	1	csuc	⊢ suc 3o
3	0 2	wceq	⊢ 4o = suc 3o