Theorem 1oex 8398

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 7671. (Revised by Zhi Wang, 19-Sep-2024.)

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

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

Syntax hints:   ∈ wcel 2109  Vcvv 3436  ∅c0 4284  {csn 4577  1_oc1o 8381

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 5235  ax-nul 5245  ax-pr 5371

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 3438  df-dif 3906  df-un 3908  df-nul 4285  df-sn 4578  df-pr 4580  df-suc 6313  df-1o 8388

This theorem is referenced by:  1on  8400  nlim2  8408  oev  8432  oe0  8440  oev2  8441  oneo  8499  nnneo  8573  enpr2d  8974  endisj  8981  map2xp  9064  snnen2o  9134  sdom1  9139  rex2dom  9142  1sdom2dom  9143  ssttrcl  9611  ttrclselem2  9622  djuexb  9805  djurcl  9807  djurf1o  9809  djuss  9816  djuun  9822  1stinr  9825  2ndinr  9826  pm54.43  9897  dju1dif  10067  djucomen  10072  djuassen  10073  infdju1  10084  pwdju1  10085  nnadju  10092  infmap2  10111  cfsuc  10151  isfin4p1  10209  dcomex  10341  pwcfsdom  10477  cfpwsdom  10478  canthp1lem2  10547  pwxpndom2  10559  indpi  10801  pinq  10821  archnq  10874  sadcf  16364  sadcp1  16366  fnpr2ob  17462  xpsfrnel  17466  xpsle  17483  setcepi  17995  setc2obas  18001  setc2ohom  18002  efgi1  19600  frgpuptinv  19650  dmdprdpr  19930  dprdpr  19931  coe1fval3  22091  00ply1bas  22122  ply1plusgfvi  22124  coe1z  22147  coe1tm  22157  ply1vscl  22269  rhmply1  22271  rhmply1vr1  22272  xpstopnlem1  23694  xpstopnlem2  23696  xpsdsval  24267  nofv  27567  noxp1o  27573  noextendlt  27579  bdayfo  27587  nosep1o  27591  nosepdmlem  27593  nolt02o  27605  nogt01o  27606  nosupbnd1lem5  27622  nosupbnd2lem1  27625  noinfno  27628  noinfbday  27630  noinfbnd1  27639  noinfbnd2lem1  27640  noinfbnd2  27641  noetasuplem1  27643  noetasuplem2  27644  noetasuplem4  27646  fply1  33493  gonanegoal  35325  fmlaomn0  35363  gonan0  35365  gonarlem  35367  gonar  35368  fmlasucdisj  35372  satffunlem  35374  satffunlem2lem1  35377  ex-sategoelel12  35400  rankeq1o  36145  bj-pr2val  36992  bj-2upln1upl  36998  rhmpsr1  42526  pw2f1ocnv  43010  omnord1ex  43277  oege2  43280  oenord1ex  43288  oenord1  43289  oaomoencom  43290  oenassex  43291  cantnfresb  43297  omcl3g  43307  clsk3nimkb  44013  clsk1indlem4  44017  clsk1indlem1  44018  f1omo  48877  f1omoOLD  48878  f1omoALT  48879  nelsubc3  49056  indthinc  49447  indthincALT  49448  prsthinc  49449  setc1obas  49477  setc1ohomfval  49478  setc1oid  49480  isinito2lem  49483  isinito3  49485  prstchom  49547  prstchom2ALT  49549  setc1onsubc  49587  cnelsubc  49589