Definition df-3o

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

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

Detailed syntax breakdown

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