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 7554 | . 2 class 2𝑜 | |
2 | c1o 7553 | . . 3 class 1𝑜 | |
3 | 2 | csuc 5725 | . 2 class suc 1𝑜 |
4 | 1, 3 | wceq 1483 | 1 wff 2𝑜 = suc 1𝑜 |
Colors of variables: wff setvar class |
This definition is referenced by: 2on 7568 2on0 7569 df2o3 7573 ondif2 7582 o1p1e2 7620 o2p2e4 7621 oneo 7661 2onn 7720 nnm2 7729 nnneo 7731 nneob 7732 snnen2o 8149 1sdom2 8159 1sdom 8163 en2 8196 pm54.43 8826 en2eleq 8831 en2other2 8832 infxpenc 8841 infxpenc2 8845 pm110.643ALT 9000 fin1a2lem4 9225 cfpwsdom 9406 canthp1lem2 9475 pwxpndom2 9487 tsk2 9587 hash2 13193 f1otrspeq 17867 pmtrf 17875 pmtrmvd 17876 pmtrfinv 17881 efgmnvl 18127 isnzr2 19263 sltval2 31809 nosgnn0 31811 sltsolem1 31826 nosepnelem 31830 nolt02o 31845 bj-2ex 32939 1oequni2o 33216 finxpreclem3 33230 finxpreclem4 33231 finxpsuclem 33234 finxp2o 33236 pw2f1ocnv 37604 pwfi2f1o 37666 clsk1indlem1 38343 |
Copyright terms: Public domain | W3C validator |