![]() |
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 | ⊢ 2o = suc 1o |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c2o 7938 | . 2 class 2o | |
2 | c1o 7937 | . . 3 class 1o | |
3 | 2 | csuc 6060 | . 2 class suc 1o |
4 | 1, 3 | wceq 1520 | 1 wff 2o = suc 1o |
Colors of variables: wff setvar class |
This definition is referenced by: 2on 7953 2oex 7954 2on0 7955 df2o3 7959 ondif2 7969 o1p1e2 8007 o2p2e4 8008 oneo 8048 2onn 8107 1one2o 8110 nnm2 8117 nnneo 8119 nneob 8120 snnen2o 8543 1sdom2 8553 1sdom 8557 en2 8590 pm54.43 9264 en2eleq 9269 en2other2 9270 infxpenc 9279 infxpenc2 9283 dju1p1e2ALT 9435 fin1a2lem4 9660 cfpwsdom 9841 canthp1lem2 9910 pwxpndom2 9922 tsk2 10022 hash2 13602 f1otrspeq 18294 pmtrf 18302 pmtrmvd 18303 pmtrfinv 18308 efgmnvl 18555 isnzr2 19713 unidifsnel 29963 unidifsnne 29964 sltval2 32717 nosgnn0 32719 sltsolem1 32734 nosepnelem 32738 nolt02o 32753 1oequni2o 34126 finxpreclem3 34151 finxpreclem4 34152 finxpsuclem 34155 finxp2o 34157 pw2f1ocnv 39070 pwfi2f1o 39132 clsk1indlem1 39831 enpr2d 40003 |
Copyright terms: Public domain | W3C validator |