| 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. Lemma 3.17 of [Schloeder] p. 10. (Contributed by NM, 18-Feb-2004.) |
| Ref | Expression |
|---|---|
| df-2o | ⊢ 2o = suc 1o |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | c2o 8500 | . 2 class 2o | |
| 2 | c1o 8499 | . . 3 class 1o | |
| 3 | 2 | csuc 6386 | . 2 class suc 1o |
| 4 | 1, 3 | wceq 1540 | 1 wff 2o = suc 1o |
| Colors of variables: wff setvar class |
| This definition is referenced by: df2o3 8514 2on 8520 2onOLD 8521 2on0 8522 ondif2 8540 o1p1e2 8578 o2p2e4 8579 oneo 8619 2onnALT 8681 1one2o 8684 nnm2 8691 nnneo 8693 nneob 8694 enpr2dOLD 9090 snnen2oOLD 9264 1sdom2ALT 9277 1sdomOLD 9285 en2 9315 pm54.43 10041 en2eleq 10048 en2other2 10049 infxpenc 10058 infxpenc2 10062 dju1p1e2ALT 10215 fin1a2lem4 10443 cfpwsdom 10624 canthp1lem2 10693 pwxpndom2 10705 tsk2 10805 hash2 14444 f1otrspeq 19465 pmtrf 19473 pmtrmvd 19474 pmtrfinv 19479 efgmnvl 19732 isnzr2 20518 sltval2 27701 nosgnn0 27703 sltsolem1 27720 nosepnelem 27724 nolt02o 27740 nogt01o 27741 unidifsnel 32553 unidifsnne 32554 ex-sategoelel12 35432 1oequni2o 37369 finxpreclem3 37394 finxpreclem4 37395 finxpsuclem 37398 finxp2o 37400 pw2f1ocnv 43049 pwfi2f1o 43108 oege2 43320 oaomoencom 43330 om2 43417 oaltom 43418 oe2 43419 omltoe 43420 nlim2NEW 43456 clsk1indlem1 44058 |
| Copyright terms: Public domain | W3C validator |