|   | 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 2141, ax-11 2157, ax-12 2177, ax-un 7755. (Revised by Zhi Wang, 19-Sep-2024.) | 
| Ref | Expression | 
|---|---|
| 1oex | ⊢ 1o ∈ V | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | df1o2 8513 | . 2 ⊢ 1o = {∅} | |
| 2 | snex 5436 | . 2 ⊢ {∅} ∈ V | |
| 3 | 1, 2 | eqeltri 2837 | 1 ⊢ 1o ∈ V | 
| Colors of variables: wff setvar class | 
| Syntax hints: ∈ wcel 2108 Vcvv 3480 ∅c0 4333 {csn 4626 1oc1o 8499 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-dif 3954 df-un 3956 df-nul 4334 df-sn 4627 df-pr 4629 df-suc 6390 df-1o 8506 | 
| This theorem is referenced by: 1on 8518 nlim2 8528 oev 8552 oe0 8560 oev2 8561 oneo 8619 nnneo 8693 enpr2d 9089 endisj 9098 map2xp 9187 snnen2o 9273 sdom1 9278 sdom1OLD 9279 rex2dom 9282 1sdom2dom 9283 1sdomOLD 9285 ssttrcl 9755 ttrclselem2 9766 djuexb 9949 djurcl 9951 djurf1o 9953 djuss 9960 djuun 9966 1stinr 9969 2ndinr 9970 pm54.43 10041 dju1dif 10213 djucomen 10218 djuassen 10219 infdju1 10230 pwdju1 10231 nnadju 10238 infmap2 10257 cfsuc 10297 isfin4p1 10355 dcomex 10487 pwcfsdom 10623 cfpwsdom 10624 canthp1lem2 10693 pwxpndom2 10705 indpi 10947 pinq 10967 archnq 11020 sadcf 16490 sadcp1 16492 fnpr2ob 17603 xpsfrnel 17607 xpsle 17624 setcepi 18133 setc2obas 18139 setc2ohom 18140 efgi1 19739 frgpuptinv 19789 dmdprdpr 20069 dprdpr 20070 coe1fval3 22210 00ply1bas 22241 ply1plusgfvi 22243 coe1z 22266 coe1tm 22276 ply1vscl 22388 rhmply1 22390 rhmply1vr1 22391 xpstopnlem1 23817 xpstopnlem2 23819 xpsdsval 24391 nofv 27702 noxp1o 27708 noextendlt 27714 bdayfo 27722 nosep1o 27726 nosepdmlem 27728 nolt02o 27740 nogt01o 27741 nosupbnd1lem5 27757 nosupbnd2lem1 27760 noinfno 27763 noinfbday 27765 noinfbnd1 27774 noinfbnd2lem1 27775 noinfbnd2 27776 noetasuplem1 27778 noetasuplem2 27779 noetasuplem4 27781 fply1 33584 gonanegoal 35357 fmlaomn0 35395 gonan0 35397 gonarlem 35399 gonar 35400 fmlasucdisj 35404 satffunlem 35406 satffunlem2lem1 35409 ex-sategoelel12 35432 rankeq1o 36172 bj-pr2val 37019 bj-2upln1upl 37025 rhmpsr1 42563 pw2f1ocnv 43049 omnord1ex 43317 oege2 43320 oenord1ex 43328 oenord1 43329 oaomoencom 43330 oenassex 43331 cantnfresb 43337 omcl3g 43347 clsk3nimkb 44053 clsk1indlem4 44057 clsk1indlem1 44058 f1omo 48792 f1omoALT 48793 indthinc 49109 indthincALT 49110 prsthinc 49111 prstchom 49166 prstchom2ALT 49168 | 
| Copyright terms: Public domain | W3C validator |