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 8096 | . 2 class 2o | |
2 | c1o 8095 | . . 3 class 1o | |
3 | 2 | csuc 6193 | . 2 class suc 1o |
4 | 1, 3 | wceq 1537 | 1 wff 2o = suc 1o |
Colors of variables: wff setvar class |
This definition is referenced by: 2on 8111 2oex 8112 2on0 8113 df2o3 8117 ondif2 8127 o1p1e2 8165 o2p2e4 8166 o2p2e4OLD 8167 oneo 8207 2onn 8266 1one2o 8269 nnm2 8276 nnneo 8278 nneob 8279 enpr2d 8597 snnen2o 8707 1sdom2 8717 1sdom 8721 en2 8754 pm54.43 9429 en2eleq 9434 en2other2 9435 infxpenc 9444 infxpenc2 9448 dju1p1e2ALT 9600 fin1a2lem4 9825 cfpwsdom 10006 canthp1lem2 10075 pwxpndom2 10087 tsk2 10187 hash2 13767 f1otrspeq 18575 pmtrf 18583 pmtrmvd 18584 pmtrfinv 18589 efgmnvl 18840 isnzr2 20036 unidifsnel 30295 unidifsnne 30296 ex-sategoelel12 32674 sltval2 33163 nosgnn0 33165 sltsolem1 33180 nosepnelem 33184 nolt02o 33199 1oequni2o 34652 finxpreclem3 34677 finxpreclem4 34678 finxpsuclem 34681 finxp2o 34683 pw2f1ocnv 39683 pwfi2f1o 39745 clsk1indlem1 40444 |
Copyright terms: Public domain | W3C validator |