Metamath Proof Explorer


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