![]() |
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 2130, ax-11 2147, ax-12 2167, ax-un 7738. (Revised by Zhi Wang, 19-Sep-2024.) |
Ref | Expression |
---|---|
1oex | ⊢ 1o ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df1o2 8495 | . 2 ⊢ 1o = {∅} | |
2 | snex 5429 | . 2 ⊢ {∅} ∈ V | |
3 | 1, 2 | eqeltri 2822 | 1 ⊢ 1o ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2099 Vcvv 3462 ∅c0 4322 {csn 4623 1oc1o 8481 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 ax-sep 5296 ax-nul 5303 ax-pr 5425 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-v 3464 df-dif 3949 df-un 3951 df-nul 4323 df-sn 4624 df-pr 4626 df-suc 6374 df-1o 8488 |
This theorem is referenced by: 1on 8500 2oexOLD 8509 nlim2 8512 oev 8536 oe0 8544 oev2 8545 oneo 8603 nnneo 8677 enpr2d 9079 endisj 9088 map2xp 9177 snnen2o 9264 sdom1 9269 sdom1OLD 9270 rex2dom 9273 1sdom2dom 9274 1sdomOLD 9276 ssttrcl 9751 ttrclselem2 9762 djuexb 9945 djurcl 9947 djurf1o 9949 djuss 9956 djuun 9962 1stinr 9965 2ndinr 9966 pm54.43 10037 dju1dif 10208 djucomen 10213 djuassen 10214 infdju1 10225 pwdju1 10226 nnadju 10233 infmap2 10252 cfsuc 10291 isfin4p1 10349 dcomex 10481 pwcfsdom 10617 cfpwsdom 10618 canthp1lem2 10687 pwxpndom2 10699 indpi 10941 pinq 10961 archnq 11014 sadcf 16448 sadcp1 16450 fnpr2ob 17568 xpsfrnel 17572 xpsle 17589 setcepi 18105 setc2obas 18111 setc2ohom 18112 efgi1 19715 frgpuptinv 19765 dmdprdpr 20045 dprdpr 20046 coe1fval3 22194 00ply1bas 22225 ply1plusgfvi 22227 coe1z 22250 coe1tm 22260 ply1vscl 22372 rhmply1 22374 rhmply1vr1 22375 xpstopnlem1 23801 xpstopnlem2 23803 xpsdsval 24375 nofv 27684 noxp1o 27690 noextendlt 27696 bdayfo 27704 nosep1o 27708 nosepdmlem 27710 nolt02o 27722 nogt01o 27723 nosupbnd1lem5 27739 nosupbnd2lem1 27742 noinfno 27745 noinfbday 27747 noinfbnd1 27756 noinfbnd2lem1 27757 noinfbnd2 27758 noetasuplem1 27760 noetasuplem2 27761 noetasuplem4 27763 fply1 33437 gonanegoal 35193 fmlaomn0 35231 gonan0 35233 gonarlem 35235 gonar 35236 fmlasucdisj 35240 satffunlem 35242 satffunlem2lem1 35245 ex-sategoelel12 35268 rankeq1o 36008 bj-pr2val 36738 bj-2upln1upl 36744 rhmpsr1 42243 pw2f1ocnv 42732 omnord1ex 43007 oege2 43010 oenord1ex 43018 oenord1 43019 oaomoencom 43020 oenassex 43021 cantnfresb 43027 omcl3g 43037 clsk3nimkb 43744 clsk1indlem4 43748 clsk1indlem1 43749 f1omo 48264 f1omoALT 48265 indthinc 48409 indthincALT 48410 prsthinc 48411 prstchom 48434 prstchom2ALT 48436 |
Copyright terms: Public domain | W3C validator |