![]() |
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. (Contributed by NM, 4-Nov-2002.) |
Ref | Expression |
---|---|
df1o2 | ⊢ 1o = {∅} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-1o 7907 | . 2 ⊢ 1o = suc ∅ | |
2 | suc0 6105 | . 2 ⊢ suc ∅ = {∅} | |
3 | 1, 2 | eqtri 2802 | 1 ⊢ 1o = {∅} |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1507 ∅c0 4180 {csn 4442 suc csuc 6033 1oc1o 7900 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2750 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-v 3417 df-dif 3834 df-un 3836 df-nul 4181 df-suc 6037 df-1o 7907 |
This theorem is referenced by: df2o3 7921 df2o2 7922 1n0 7923 el1o 7928 dif1o 7929 0we1 7935 oeeui 8031 map0e 8247 ensn1 8372 en1 8375 map1 8391 xp1en 8401 pwfi 8616 infxpenlem 9235 fseqenlem1 9246 dju1dif 9398 infdju1 9415 pwdju1 9416 infmap2 9440 cflim2 9485 pwxpndom2 9887 pwdjundom 9889 gchxpidm 9891 wuncval2 9969 tsk1 9986 hashen1 13548 sylow2alem2 18507 psr1baslem 20059 fvcoe1 20081 coe1f2 20083 coe1sfi 20087 coe1add 20138 coe1mul2lem1 20141 coe1mul2lem2 20142 coe1mul2 20143 coe1tm 20147 ply1coe 20170 evls1rhmlem 20190 evl1sca 20202 evl1var 20204 pf1mpf 20220 pf1ind 20223 mat0dimbas0 20782 mavmul0g 20869 hmph0 22110 tdeglem2 24361 deg1ldg 24392 deg1leb 24395 deg1val 24396 fply1 30604 bnj105 31642 bnj96 31784 bnj98 31786 bnj149 31794 rankeq1o 33153 ordcmp 33315 ssoninhaus 33316 onint1 33317 poimirlem28 34361 reheibor 34559 wopprc 39023 pwslnmlem0 39087 pwfi2f1o 39092 lincval0 43838 lco0 43850 linds0 43888 |
Copyright terms: Public domain | W3C validator |