![]() |
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 | ⊢ 2𝑜 = suc 1𝑜 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c2o 7599 | . 2 class 2𝑜 | |
2 | c1o 7598 | . . 3 class 1𝑜 | |
3 | 2 | csuc 5763 | . 2 class suc 1𝑜 |
4 | 1, 3 | wceq 1523 | 1 wff 2𝑜 = suc 1𝑜 |
Colors of variables: wff setvar class |
This definition is referenced by: 2on 7613 2on0 7614 df2o3 7618 ondif2 7627 o1p1e2 7665 o2p2e4 7666 oneo 7706 2onn 7765 nnm2 7774 nnneo 7776 nneob 7777 snnen2o 8190 1sdom2 8200 1sdom 8204 en2 8237 pm54.43 8864 en2eleq 8869 en2other2 8870 infxpenc 8879 infxpenc2 8883 pm110.643ALT 9038 fin1a2lem4 9263 cfpwsdom 9444 canthp1lem2 9513 pwxpndom2 9525 tsk2 9625 hash2 13231 f1otrspeq 17913 pmtrf 17921 pmtrmvd 17922 pmtrfinv 17927 efgmnvl 18173 isnzr2 19311 sltval2 31934 nosgnn0 31936 sltsolem1 31951 nosepnelem 31955 nolt02o 31970 bj-2ex 33064 1oequni2o 33346 finxpreclem3 33360 finxpreclem4 33361 finxpsuclem 33364 finxp2o 33366 pw2f1ocnv 37921 pwfi2f1o 37983 clsk1indlem1 38660 |
Copyright terms: Public domain | W3C validator |