Theorem 1oex 8462

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

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

Step	Hyp	Ref	Expression
1		df1o2 8459	. 2 ⊢ 1o = {∅}
2		snex 5411	. 2 ⊢ {∅} ∈ V
3	1, 2	eqeltri 2865	1 ⊢ 1o ∈ V

Syntax hints:   ∈ wcel 2149  Vcvv 3463  ∅c0 4294  {csn 4594  1_oc1o 8445

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-dif 3916  df-un 3918  df-nul 4295  df-sn 4595  df-pr 4597  df-suc 6367  df-1o 8452

This theorem is referenced by:  1oelpr  8463  1on  8465  nlim2  8474  oev  8498  oe0  8506  oev2  8507  oneo  8565  nnneo  8640  enpr2d  9044  endisj  9051  map2xp  9134  snnen2o  9204  sdom1  9209  rex2dom  9212  1sdom2dom  9213  ssttrcl  9683  ttrclselem2  9694  djuexb  9894  djurcl  9896  djurf1o  9898  djuss  9905  djuun  9911  1stinr  9914  2ndinr  9915  pm54.43  9986  dju1dif  10155  djucomen  10160  djuassen  10161  infdju1  10172  pwdju1  10173  nnadju  10180  infmap2  10199  cfsuc  10240  isfin4p1  10298  dcomex  10430  pwcfsdom  10567  cfpwsdom  10568  canthp1lem2  10637  pwxpndom2  10649  indpi  10891  pinq  10911  archnq  10964  sadcf  16510  sadcp1  16512  fnpr2ob  17611  xpsfrnel  17615  xpsle  17632  setcepi  18144  setc2obas  18150  setc2ohom  18151  efgi1  19790  frgpuptinv  19840  dmdprdpr  20120  dprdpr  20121  coe1fval3  22336  00ply1bas  22367  ply1plusgfvi  22369  coe1z  22392  coe1tm  22402  ply1vscl  22509  rhmply1  22511  rhmply1vr1  22512  xpstopnlem1  23934  xpstopnlem2  23936  xpsdsval  24506  nofv  27786  noxp1o  27792  noextendlt  27798  bdayfo  27806  nosep1o  27810  nosepdmlem  27812  nolt02o  27824  nogt01o  27825  nosupbnd1lem5  27841  nosupbnd2lem1  27844  noinfno  27847  noinfbday  27849  noinfbnd1  27858  noinfbnd2lem1  27859  noinfbnd2  27860  noetasuplem1  27862  noetasuplem2  27863  noetasuplem4  27865  fply1  33792  selvply1rhmlema  33852  selvply1rhmlemb  33853  selvply1rhmlem1  33854  selvply1rhmlem2  33855  selvply1rhmlem4  33857  selvply1rhm0  33860  gonanegoal  35742  fmlaomn0  35780  gonan0  35782  gonarlem  35784  gonar  35785  fmlasucdisj  35789  satffunlem  35791  satffunlem2lem1  35794  ex-sategoelel12  35817  rankeq1o  36561  bj-pr2val  37541  bj-2upln1upl  37547  rhmpsr1  43207  pw2f1ocnv  43655  omnord1ex  43922  oege2  43925  oenord1ex  43933  oenord1  43934  oenassex  43936  cantnfresb  43942  omcl3g  43952  clsk3nimkb  44657  clsk1indlem4  44661  clsk1indlem1  44662  f1omo  49555  f1omoOLD  49556  f1omoALT  49557  nelsubc3  49733  indthinc  50124  indthincALT  50125  prsthinc  50126  setc1obas  50154  setc1ohomfval  50155  setc1oid  50157  isinito2lem  50160  isinito3  50162  prstchom  50224  prstchom2ALT  50226  setc1onsubc  50264  cnelsubc  50266