![]() |
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 8456 | . 2 class 2o | |
2 | c1o 8455 | . . 3 class 1o | |
3 | 2 | csuc 6357 | . 2 class suc 1o |
4 | 1, 3 | wceq 1533 | 1 wff 2o = suc 1o |
Colors of variables: wff setvar class |
This definition is referenced by: df2o3 8470 2on 8476 2onOLD 8477 2on0 8478 2oexOLD 8483 ondif2 8498 o1p1e2 8536 o2p2e4 8537 oneo 8577 2onnALT 8639 1one2o 8642 nnm2 8649 nnneo 8651 nneob 8652 enpr2dOLD 9047 snnen2oOLD 9224 1sdom2ALT 9238 1sdomOLD 9246 en2 9278 pm54.43 9993 en2eleq 10000 en2other2 10001 infxpenc 10010 infxpenc2 10014 dju1p1e2ALT 10166 fin1a2lem4 10395 cfpwsdom 10576 canthp1lem2 10645 pwxpndom2 10657 tsk2 10757 hash2 14363 f1otrspeq 19359 pmtrf 19367 pmtrmvd 19368 pmtrfinv 19373 efgmnvl 19626 isnzr2 20412 sltval2 27508 nosgnn0 27510 sltsolem1 27527 nosepnelem 27531 nolt02o 27547 nogt01o 27548 unidifsnel 32244 unidifsnne 32245 ex-sategoelel12 34909 1oequni2o 36740 finxpreclem3 36765 finxpreclem4 36766 finxpsuclem 36769 finxp2o 36771 pw2f1ocnv 42290 pwfi2f1o 42352 oege2 42571 oaomoencom 42581 om2 42669 oaltom 42670 oe2 42671 omltoe 42672 nlim2NEW 42708 clsk1indlem1 43310 |
Copyright terms: Public domain | W3C validator |