Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-2o | Structured version Visualization version GIF version |
Description: Define the ordinal number 2. (Contributed by NM, 18-Feb-2004.) |
Ref | Expression |
---|---|
df-2o | ⊢ 2𝑜 = suc 1𝑜 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c2o 7441 | . 2 class 2𝑜 | |
2 | c1o 7440 | . . 3 class 1𝑜 | |
3 | 2 | csuc 5642 | . 2 class suc 1𝑜 |
4 | 1, 3 | wceq 1475 | 1 wff 2𝑜 = suc 1𝑜 |
Colors of variables: wff setvar class |
This definition is referenced by: 2on 7455 2on0 7456 df2o3 7460 ondif2 7469 o1p1e2 7507 o2p2e4 7508 oneo 7548 2onn 7607 nnm2 7616 nnneo 7618 nneob 7619 snnen2o 8034 1sdom2 8044 1sdom 8048 en2 8081 pm54.43 8709 en2eleq 8714 en2other2 8715 infxpenc 8724 infxpenc2 8728 pm110.643ALT 8883 fin1a2lem4 9108 cfpwsdom 9285 canthp1lem2 9354 pwxpndom2 9366 tsk2 9466 hash2 13054 f1otrspeq 17690 pmtrf 17698 pmtrmvd 17699 pmtrfinv 17704 efgmnvl 17950 isnzr2 19084 sltval2 31053 nosgnn0 31055 sltsolem1 31067 bj-2ex 32132 1oequni2o 32392 finxpreclem3 32406 finxpreclem4 32407 finxpsuclem 32410 finxp2o 32412 pw2f1ocnv 36622 pwfi2f1o 36684 clsk1indlem1 37363 |
Copyright terms: Public domain | W3C validator |