Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > df-3o | Structured version Visualization version GIF version | ||
| Description: Define the ordinal number 3. (Contributed by Mario Carneiro, 14-Jul-2013.) |
| Ref | Expression |
|---|---|
| df-3o | ⊢ 3o = suc 2o |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | c3o 8475 | . 2 class 3o | |
| 2 | c2o 8474 | . . 3 class 2o | |
| 3 | 2 | csuc 6364 | . 2 class suc 2o |
| 4 | 1, 3 | wceq 1569 | 1 wff 3o = suc 2o |
| Colors of variables: wff setvar class |
| This definition is used by: ord3 8496 3on 8497 o2p2e4 8553 3onn 8657 en3 9276 hash3 14554 finxp3o 38417 df3o2 44409 df3o3 44410 omcl3g 44430 nlim3 44539 tr3dom 44623 har2o 44641 clsk1independent 45140 par2catid 50861 parswapprop 50871 |
| Copyright terms: Public domain | W3C validator |