Theorem 1oex 8405

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

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

Step	Hyp	Ref	Expression
1		df1o2 8402	. 2 ⊢ 1o = {∅}
2		snex 5379	. 2 ⊢ {∅} ∈ V
3	1, 2	eqeltri 2830	1 ⊢ 1o ∈ V

Syntax hints:   ∈ wcel 2113  Vcvv 3438  ∅c0 4283  {csn 4578  1_oc1o 8388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-dif 3902  df-un 3904  df-nul 4284  df-sn 4579  df-pr 4581  df-suc 6321  df-1o 8395

This theorem is referenced by:  1on  8407  nlim2  8415  oev  8439  oe0  8447  oev2  8448  oneo  8506  nnneo  8581  enpr2d  8983  endisj  8990  map2xp  9073  snnen2o  9143  sdom1  9148  rex2dom  9151  1sdom2dom  9152  ssttrcl  9622  ttrclselem2  9633  djuexb  9819  djurcl  9821  djurf1o  9823  djuss  9830  djuun  9836  1stinr  9839  2ndinr  9840  pm54.43  9911  dju1dif  10081  djucomen  10086  djuassen  10087  infdju1  10098  pwdju1  10099  nnadju  10106  infmap2  10125  cfsuc  10165  isfin4p1  10223  dcomex  10355  pwcfsdom  10492  cfpwsdom  10493  canthp1lem2  10562  pwxpndom2  10574  indpi  10816  pinq  10836  archnq  10889  sadcf  16378  sadcp1  16380  fnpr2ob  17477  xpsfrnel  17481  xpsle  17498  setcepi  18010  setc2obas  18016  setc2ohom  18017  efgi1  19648  frgpuptinv  19698  dmdprdpr  19978  dprdpr  19979  coe1fval3  22147  00ply1bas  22178  ply1plusgfvi  22180  coe1z  22203  coe1tm  22213  ply1vscl  22326  rhmply1  22328  rhmply1vr1  22329  xpstopnlem1  23751  xpstopnlem2  23753  xpsdsval  24323  nofv  27623  noxp1o  27629  noextendlt  27635  bdayfo  27643  nosep1o  27647  nosepdmlem  27649  nolt02o  27661  nogt01o  27662  nosupbnd1lem5  27678  nosupbnd2lem1  27681  noinfno  27684  noinfbday  27686  noinfbnd1  27695  noinfbnd2lem1  27696  noinfbnd2  27697  noetasuplem1  27699  noetasuplem2  27700  noetasuplem4  27702  fply1  33588  gonanegoal  35495  fmlaomn0  35533  gonan0  35535  gonarlem  35537  gonar  35538  fmlasucdisj  35542  satffunlem  35544  satffunlem2lem1  35547  ex-sategoelel12  35570  rankeq1o  36314  bj-pr2val  37162  bj-2upln1upl  37168  rhmpsr1  42748  pw2f1ocnv  43221  omnord1ex  43488  oege2  43491  oenord1ex  43499  oenord1  43500  oaomoencom  43501  oenassex  43502  cantnfresb  43508  omcl3g  43518  clsk3nimkb  44223  clsk1indlem4  44227  clsk1indlem1  44228  f1omo  49080  f1omoOLD  49081  f1omoALT  49082  nelsubc3  49258  indthinc  49649  indthincALT  49650  prsthinc  49651  setc1obas  49679  setc1ohomfval  49680  setc1oid  49682  isinito2lem  49685  isinito3  49687  prstchom  49749  prstchom2ALT  49751  setc1onsubc  49789  cnelsubc  49791