![]() |
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 | ⊢ 1𝑜 = {∅} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-1o 7713 | . 2 ⊢ 1𝑜 = suc ∅ | |
2 | suc0 5942 | . 2 ⊢ suc ∅ = {∅} | |
3 | 1, 2 | eqtri 2793 | 1 ⊢ 1𝑜 = {∅} |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1631 ∅c0 4063 {csn 4316 suc csuc 5868 1𝑜c1o 7706 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 835 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-v 3353 df-dif 3726 df-un 3728 df-nul 4064 df-suc 5872 df-1o 7713 |
This theorem is referenced by: df2o3 7727 df2o2 7728 1n0 7729 el1o 7733 dif1o 7734 0we1 7740 oeeui 7836 map0e 8047 ensn1 8173 en1 8176 map1 8192 xp1en 8202 pwfi 8417 infxpenlem 9036 fseqenlem1 9047 cda1dif 9200 infcda1 9217 pwcda1 9218 infmap2 9242 cflim2 9287 pwxpndom2 9689 pwcdandom 9691 gchxpidm 9693 wuncval2 9771 tsk1 9788 hashen1 13362 sylow2alem2 18240 psr1baslem 19770 fvcoe1 19792 coe1f2 19794 coe1sfi 19798 coe1add 19849 coe1mul2lem1 19852 coe1mul2lem2 19853 coe1mul2 19854 coe1tm 19858 ply1coe 19881 evls1rhmlem 19901 evl1sca 19913 evl1var 19915 pf1mpf 19931 pf1ind 19934 mat0dimbas0 20490 mavmul0g 20577 hmph0 21819 tdeglem2 24041 deg1ldg 24072 deg1leb 24075 deg1val 24076 bnj105 31130 bnj96 31273 bnj98 31275 bnj149 31283 rankeq1o 32615 ordcmp 32783 ssoninhaus 32784 onint1 32785 poimirlem28 33770 reheibor 33970 wopprc 38123 pwslnmlem0 38187 pwfi2f1o 38192 lincval0 42732 lco0 42744 linds0 42782 |
Copyright terms: Public domain | W3C validator |