Theorem 1oex 8421

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

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

Step	Hyp	Ref	Expression
1		df1o2 8418	. 2 ⊢ 1o = {∅}
2		snex 5386	. 2 ⊢ {∅} ∈ V
3	1, 2	eqeltri 2824	1 ⊢ 1o ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3444  ∅c0 4292  {csn 4585  1_oc1o 8404

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-dif 3914  df-un 3916  df-nul 4293  df-sn 4586  df-pr 4588  df-suc 6326  df-1o 8411

This theorem is referenced by:  1on  8423  nlim2  8431  oev  8455  oe0  8463  oev2  8464  oneo  8522  nnneo  8596  enpr2d  8997  endisj  9005  map2xp  9088  snnen2o  9161  sdom1  9166  rex2dom  9169  1sdom2dom  9170  1sdomOLD  9172  ssttrcl  9644  ttrclselem2  9655  djuexb  9838  djurcl  9840  djurf1o  9842  djuss  9849  djuun  9855  1stinr  9858  2ndinr  9859  pm54.43  9930  dju1dif  10102  djucomen  10107  djuassen  10108  infdju1  10119  pwdju1  10120  nnadju  10127  infmap2  10146  cfsuc  10186  isfin4p1  10244  dcomex  10376  pwcfsdom  10512  cfpwsdom  10513  canthp1lem2  10582  pwxpndom2  10594  indpi  10836  pinq  10856  archnq  10909  sadcf  16399  sadcp1  16401  fnpr2ob  17497  xpsfrnel  17501  xpsle  17518  setcepi  18030  setc2obas  18036  setc2ohom  18037  efgi1  19635  frgpuptinv  19685  dmdprdpr  19965  dprdpr  19966  coe1fval3  22126  00ply1bas  22157  ply1plusgfvi  22159  coe1z  22182  coe1tm  22192  ply1vscl  22304  rhmply1  22306  rhmply1vr1  22307  xpstopnlem1  23729  xpstopnlem2  23731  xpsdsval  24302  nofv  27602  noxp1o  27608  noextendlt  27614  bdayfo  27622  nosep1o  27626  nosepdmlem  27628  nolt02o  27640  nogt01o  27641  nosupbnd1lem5  27657  nosupbnd2lem1  27660  noinfno  27663  noinfbday  27665  noinfbnd1  27674  noinfbnd2lem1  27675  noinfbnd2  27676  noetasuplem1  27678  noetasuplem2  27679  noetasuplem4  27681  fply1  33520  gonanegoal  35332  fmlaomn0  35370  gonan0  35372  gonarlem  35374  gonar  35375  fmlasucdisj  35379  satffunlem  35381  satffunlem2lem1  35384  ex-sategoelel12  35407  rankeq1o  36152  bj-pr2val  36999  bj-2upln1upl  37005  rhmpsr1  42534  pw2f1ocnv  43019  omnord1ex  43286  oege2  43289  oenord1ex  43297  oenord1  43298  oaomoencom  43299  oenassex  43300  cantnfresb  43306  omcl3g  43316  clsk3nimkb  44022  clsk1indlem4  44026  clsk1indlem1  44027  f1omo  48874  f1omoOLD  48875  f1omoALT  48876  nelsubc3  49053  indthinc  49444  indthincALT  49445  prsthinc  49446  setc1obas  49474  setc1ohomfval  49475  setc1oid  49477  isinito2lem  49480  isinito3  49482  prstchom  49544  prstchom2ALT  49546  setc1onsubc  49584  cnelsubc  49586