![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 1oex | Structured version Visualization version GIF version |
Description: Ordinal 1 is a set. (Contributed by BJ, 6-Apr-2019.) (Proof shortened by AV, 1-Jul-2022.) Remove dependency on ax-10 2138, ax-11 2155, ax-12 2172, ax-un 7673. (Revised by Zhi Wang, 19-Sep-2024.) |
Ref | Expression |
---|---|
1oex | ⊢ 1o ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df1o2 8420 | . 2 ⊢ 1o = {∅} | |
2 | snex 5389 | . 2 ⊢ {∅} ∈ V | |
3 | 1, 2 | eqeltri 2834 | 1 ⊢ 1o ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 Vcvv 3446 ∅c0 4283 {csn 4587 1oc1o 8406 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 ax-sep 5257 ax-nul 5264 ax-pr 5385 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-v 3448 df-dif 3914 df-un 3916 df-nul 4284 df-sn 4588 df-pr 4590 df-suc 6324 df-1o 8413 |
This theorem is referenced by: 1on 8425 2oexOLD 8434 nlim2 8437 oev 8461 oe0 8469 oev2 8470 oneo 8529 nnneo 8602 enpr2d 8994 endisj 9003 map2xp 9092 snnen2o 9182 sdom1 9187 sdom1OLD 9188 rex2dom 9191 1sdom2dom 9192 1sdomOLD 9194 ssttrcl 9652 ttrclselem2 9663 djuexb 9846 djurcl 9848 djurf1o 9850 djuss 9857 djuun 9863 1stinr 9866 2ndinr 9867 pm54.43 9938 dju1dif 10109 djucomen 10114 djuassen 10115 infdju1 10126 pwdju1 10127 nnadju 10134 infmap2 10155 cfsuc 10194 isfin4p1 10252 dcomex 10384 pwcfsdom 10520 cfpwsdom 10521 canthp1lem2 10590 pwxpndom2 10602 indpi 10844 pinq 10864 archnq 10917 sadcf 16334 sadcp1 16336 fnpr2ob 17441 xpsfrnel 17445 xpsle 17462 setcepi 17975 setc2obas 17981 setc2ohom 17982 efgi1 19504 frgpuptinv 19554 dmdprdpr 19829 dprdpr 19830 coe1fval3 21582 00ply1bas 21614 ply1plusgfvi 21616 coe1z 21637 coe1tm 21647 xpstopnlem1 23163 xpstopnlem2 23165 xpsdsval 23737 nofv 27008 noxp1o 27014 noextendlt 27020 bdayfo 27028 nosep1o 27032 nosepdmlem 27034 nolt02o 27046 nogt01o 27047 nosupbnd1lem5 27063 nosupbnd2lem1 27066 noinfno 27069 noinfbday 27071 noinfbnd1 27080 noinfbnd2lem1 27081 noinfbnd2 27082 noetasuplem1 27084 noetasuplem2 27085 noetasuplem4 27087 fply1 32268 gonanegoal 33949 fmlaomn0 33987 gonan0 33989 gonarlem 33991 gonar 33992 fmlasucdisj 33996 satffunlem 33998 satffunlem2lem1 34001 ex-sategoelel12 34024 rankeq1o 34759 bj-pr2val 35492 bj-2upln1upl 35498 pw2f1ocnv 41364 omnord1ex 41641 oege2 41644 oenord1ex 41652 oenord1 41653 oaomoencom 41654 oenassex 41655 cantnfresb 41661 omcl3g 41670 clsk3nimkb 42319 clsk1indlem4 42323 clsk1indlem1 42324 f1omo 46934 f1omoALT 46935 indthinc 47079 indthincALT 47080 prsthinc 47081 prstchom 47104 prstchom2ALT 47106 |
Copyright terms: Public domain | W3C validator |