Theorem 1oex 8427

Description: Ordinal 1 is a set. (Contributed by BJ, 6-Apr-2019.) (Proof shortened by AV, 1-Jul-2022.) Remove dependency on ax-10 2137, ax-11 2154, ax-12 2171, ax-un 7677. (Revised by Zhi Wang, 19-Sep-2024.)

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

Step	Hyp	Ref	Expression
1		df1o2 8424	. 2 ⊢ 1o = {∅}
2		snex 5393	. 2 ⊢ {∅} ∈ V
3	1, 2	eqeltri 2828	1 ⊢ 1o ∈ V

Syntax hints:   ∈ wcel 2106  Vcvv 3446  ∅c0 4287  {csn 4591  1_oc1o 8410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-dif 3916  df-un 3918  df-nul 4288  df-sn 4592  df-pr 4594  df-suc 6328  df-1o 8417

This theorem is referenced by:  1on  8429  2oexOLD  8438  nlim2  8441  oev  8465  oe0  8473  oev2  8474  oneo  8533  nnneo  8606  enpr2d  9000  endisj  9009  map2xp  9098  snnen2o  9188  sdom1  9193  sdom1OLD  9194  rex2dom  9197  1sdom2dom  9198  1sdomOLD  9200  ssttrcl  9660  ttrclselem2  9671  djuexb  9854  djurcl  9856  djurf1o  9858  djuss  9865  djuun  9871  1stinr  9874  2ndinr  9875  pm54.43  9946  dju1dif  10117  djucomen  10122  djuassen  10123  infdju1  10134  pwdju1  10135  nnadju  10142  infmap2  10163  cfsuc  10202  isfin4p1  10260  dcomex  10392  pwcfsdom  10528  cfpwsdom  10529  canthp1lem2  10598  pwxpndom2  10610  indpi  10852  pinq  10872  archnq  10925  sadcf  16344  sadcp1  16346  fnpr2ob  17454  xpsfrnel  17458  xpsle  17475  setcepi  17988  setc2obas  17994  setc2ohom  17995  efgi1  19517  frgpuptinv  19567  dmdprdpr  19842  dprdpr  19843  coe1fval3  21616  00ply1bas  21648  ply1plusgfvi  21650  coe1z  21671  coe1tm  21681  xpstopnlem1  23197  xpstopnlem2  23199  xpsdsval  23771  nofv  27042  noxp1o  27048  noextendlt  27054  bdayfo  27062  nosep1o  27066  nosepdmlem  27068  nolt02o  27080  nogt01o  27081  nosupbnd1lem5  27097  nosupbnd2lem1  27100  noinfno  27103  noinfbday  27105  noinfbnd1  27114  noinfbnd2lem1  27115  noinfbnd2  27116  noetasuplem1  27118  noetasuplem2  27119  noetasuplem4  27121  fply1  32341  gonanegoal  34033  fmlaomn0  34071  gonan0  34073  gonarlem  34075  gonar  34076  fmlasucdisj  34080  satffunlem  34082  satffunlem2lem1  34085  ex-sategoelel12  34108  rankeq1o  34832  bj-pr2val  35562  bj-2upln1upl  35568  pw2f1ocnv  41419  omnord1ex  41697  oege2  41700  oenord1ex  41708  oenord1  41709  oaomoencom  41710  oenassex  41711  cantnfresb  41717  omcl3g  41727  clsk3nimkb  42434  clsk1indlem4  42438  clsk1indlem1  42439  f1omo  47047  f1omoALT  47048  indthinc  47192  indthincALT  47193  prsthinc  47194  prstchom  47217  prstchom2ALT  47219