Theorem 1oex 8417

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

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

Step	Hyp	Ref	Expression
1		df1o2 8414	. 2 ⊢ 1o = {∅}
2		snex 5385	. 2 ⊢ {∅} ∈ V
3	1, 2	eqeltri 2833	1 ⊢ 1o ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3442  ∅c0 4287  {csn 4582  1_oc1o 8400

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-dif 3906  df-un 3908  df-nul 4288  df-sn 4583  df-pr 4585  df-suc 6331  df-1o 8407

This theorem is referenced by:  1on  8419  nlim2  8427  oev  8451  oe0  8459  oev2  8460  oneo  8518  nnneo  8593  enpr2d  8997  endisj  9004  map2xp  9087  snnen2o  9157  sdom1  9162  rex2dom  9165  1sdom2dom  9166  ssttrcl  9636  ttrclselem2  9647  djuexb  9833  djurcl  9835  djurf1o  9837  djuss  9844  djuun  9850  1stinr  9853  2ndinr  9854  pm54.43  9925  dju1dif  10095  djucomen  10100  djuassen  10101  infdju1  10112  pwdju1  10113  nnadju  10120  infmap2  10139  cfsuc  10179  isfin4p1  10237  dcomex  10369  pwcfsdom  10506  cfpwsdom  10507  canthp1lem2  10576  pwxpndom2  10588  indpi  10830  pinq  10850  archnq  10903  sadcf  16392  sadcp1  16394  fnpr2ob  17491  xpsfrnel  17495  xpsle  17512  setcepi  18024  setc2obas  18030  setc2ohom  18031  efgi1  19662  frgpuptinv  19712  dmdprdpr  19992  dprdpr  19993  coe1fval3  22161  00ply1bas  22192  ply1plusgfvi  22194  coe1z  22217  coe1tm  22227  ply1vscl  22340  rhmply1  22342  rhmply1vr1  22343  xpstopnlem1  23765  xpstopnlem2  23767  xpsdsval  24337  nofv  27637  noxp1o  27643  noextendlt  27649  bdayfo  27657  nosep1o  27661  nosepdmlem  27663  nolt02o  27675  nogt01o  27676  nosupbnd1lem5  27692  nosupbnd2lem1  27695  noinfno  27698  noinfbday  27700  noinfbnd1  27709  noinfbnd2lem1  27710  noinfbnd2  27711  noetasuplem1  27713  noetasuplem2  27714  noetasuplem4  27716  fply1  33651  gonanegoal  35568  fmlaomn0  35606  gonan0  35608  gonarlem  35610  gonar  35611  fmlasucdisj  35615  satffunlem  35617  satffunlem2lem1  35620  ex-sategoelel12  35643  rankeq1o  36387  bj-pr2val  37266  bj-2upln1upl  37272  rhmpsr1  42921  pw2f1ocnv  43394  omnord1ex  43661  oege2  43664  oenord1ex  43672  oenord1  43673  oaomoencom  43674  oenassex  43675  cantnfresb  43681  omcl3g  43691  clsk3nimkb  44396  clsk1indlem4  44400  clsk1indlem1  44401  f1omo  49252  f1omoOLD  49253  f1omoALT  49254  nelsubc3  49430  indthinc  49821  indthincALT  49822  prsthinc  49823  setc1obas  49851  setc1ohomfval  49852  setc1oid  49854  isinito2lem  49857  isinito3  49859  prstchom  49921  prstchom2ALT  49923  setc1onsubc  49961  cnelsubc  49963