Description: Define the ordinal number 3. (Contributed by Mario Carneiro, 14-Jul-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | df-3o | |- 3o = suc 2o |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | c3o | |- 3o |
|
1 | c2o | |- 2o |
|
2 | 1 | csuc | |- suc 2o |
3 | 0 2 | wceq | |- 3o = suc 2o |