![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df1o2 | Structured version Visualization version GIF version |
Description: Expanded value of the ordinal number 1. Definition 2.1 of [Schloeder] p. 4. (Contributed by NM, 4-Nov-2002.) |
Ref | Expression |
---|---|
df1o2 | ⊢ 1o = {∅} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-1o 8524 | . 2 ⊢ 1o = suc ∅ | |
2 | suc0 6472 | . 2 ⊢ suc ∅ = {∅} | |
3 | 1, 2 | eqtri 2768 | 1 ⊢ 1o = {∅} |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1537 ∅c0 4352 {csn 4648 suc csuc 6399 1oc1o 8517 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2711 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-tru 1540 df-fal 1550 df-ex 1778 df-sb 2065 df-clab 2718 df-cleq 2732 df-clel 2819 df-v 3490 df-dif 3979 df-un 3981 df-nul 4353 df-suc 6403 df-1o 8524 |
This theorem is referenced by: df2o3 8532 df2o2 8533 1oex 8534 1n0 8546 nlim1 8547 el1o 8553 dif1o 8558 0we1 8564 oeeui 8660 map0e 8942 ensn1 9084 ensn1OLD 9085 en1 9088 en1OLD 9089 map1 9107 xp1en 9125 0sdom1dom 9303 1sdom2 9305 sdom1 9307 1sdom2dom 9312 pwfiOLD 9419 ssttrcl 9786 ttrclss 9791 ttrclselem2 9797 infxpenlem 10084 fseqenlem1 10095 dju1dif 10244 infdju1 10261 pwdju1 10262 infmap2 10288 cflim2 10334 pwxpndom2 10736 pwdjundom 10738 gchxpidm 10740 wuncval2 10818 tsk1 10835 hashen1 14421 sylow2alem2 19662 psr1baslem 22209 fvcoe1 22232 coe1f2 22234 coe1sfi 22238 coe1add 22290 coe1mul2lem1 22293 coe1mul2lem2 22294 coe1mul2 22295 coe1tm 22299 ply1coe 22325 evls1rhmlem 22348 evl1sca 22361 evl1var 22363 pf1mpf 22379 pf1ind 22382 mat0dimbas0 22495 mavmul0g 22582 hmph0 23826 tdeglem2 26122 deg1ldg 26153 deg1leb 26156 deg1val 26157 old1 27934 fply1 33551 bnj105 34702 bnj96 34843 bnj98 34845 bnj149 34853 rankeq1o 36137 ordcmp 36415 ssoninhaus 36416 onint1 36417 poimirlem28 37610 reheibor 37801 wopprc 42989 pwslnmlem0 43050 pwfi2f1o 43055 nadd1suc 43356 lincval0 48146 lco0 48158 linds0 48196 |
Copyright terms: Public domain | W3C validator |