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 8087 | . 2 class 2o | |
2 | c1o 8086 | . . 3 class 1o | |
3 | 2 | csuc 6187 | . 2 class suc 1o |
4 | 1, 3 | wceq 1528 | 1 wff 2o = suc 1o |
Colors of variables: wff setvar class |
This definition is referenced by: 2on 8102 2oex 8103 2on0 8104 df2o3 8108 ondif2 8118 o1p1e2 8156 o2p2e4 8157 oneo 8197 2onn 8256 1one2o 8259 nnm2 8266 nnneo 8268 nneob 8269 enpr2d 8586 snnen2o 8696 1sdom2 8706 1sdom 8710 en2 8743 pm54.43 9418 en2eleq 9423 en2other2 9424 infxpenc 9433 infxpenc2 9437 dju1p1e2ALT 9589 fin1a2lem4 9814 cfpwsdom 9995 canthp1lem2 10064 pwxpndom2 10076 tsk2 10176 hash2 13756 f1otrspeq 18506 pmtrf 18514 pmtrmvd 18515 pmtrfinv 18520 efgmnvl 18771 isnzr2 19966 unidifsnel 30223 unidifsnne 30224 ex-sategoelel12 32572 sltval2 33061 nosgnn0 33063 sltsolem1 33078 nosepnelem 33082 nolt02o 33097 1oequni2o 34532 finxpreclem3 34557 finxpreclem4 34558 finxpsuclem 34561 finxp2o 34563 pw2f1ocnv 39514 pwfi2f1o 39576 clsk1indlem1 40275 |
Copyright terms: Public domain | W3C validator |