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  18026  setc2obas  18032  setc2ohom  18033  efgi1  19627  frgpuptinv  19677  dmdprdpr  19957  dprdpr  19958  coe1fval3  22069  00ply1bas  22100  ply1plusgfvi  22102  coe1z  22125  coe1tm  22135  ply1vscl  22247  rhmply1  22249  rhmply1vr1  22250  xpstopnlem1  23672  xpstopnlem2  23674  xpsdsval  24245  nofv  27545  noxp1o  27551  noextendlt  27557  bdayfo  27565  nosep1o  27569  nosepdmlem  27571  nolt02o  27583  nogt01o  27584  nosupbnd1lem5  27600  nosupbnd2lem1  27603  noinfno  27606  noinfbday  27608  noinfbnd1  27617  noinfbnd2lem1  27618  noinfbnd2  27619  noetasuplem1  27621  noetasuplem2  27622  noetasuplem4  27624  fply1  33500  gonanegoal  35312  fmlaomn0  35350  gonan0  35352  gonarlem  35354  gonar  35355  fmlasucdisj  35359  satffunlem  35361  satffunlem2lem1  35364  ex-sategoelel12  35387  rankeq1o  36132  bj-pr2val  36979  bj-2upln1upl  36985  rhmpsr1  42514  pw2f1ocnv  42999  omnord1ex  43266  oege2  43269  oenord1ex  43277  oenord1  43278  oaomoencom  43279  oenassex  43280  cantnfresb  43286  omcl3g  43296  clsk3nimkb  44002  clsk1indlem4  44006  clsk1indlem1  44007  f1omo  48854  f1omoOLD  48855  f1omoALT  48856  nelsubc3  49033  indthinc  49424  indthincALT  49425  prsthinc  49426  setc1obas  49454  setc1ohomfval  49455  setc1oid  49457  isinito2lem  49460  isinito3  49462  prstchom  49524  prstchom2ALT  49526  setc1onsubc  49564  cnelsubc  49566