Theorem 1oex 8478

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

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

Step	Hyp	Ref	Expression
1		df1o2 8475	. 2 ⊢ 1o = {∅}
2		snex 5431	. 2 ⊢ {∅} ∈ V
3	1, 2	eqeltri 2829	1 ⊢ 1o ∈ V

Syntax hints:   ∈ wcel 2106  Vcvv 3474  ∅c0 4322  {csn 4628  1_oc1o 8461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-dif 3951  df-un 3953  df-nul 4323  df-sn 4629  df-pr 4631  df-suc 6370  df-1o 8468

This theorem is referenced by:  1on  8480  2oexOLD  8489  nlim2  8492  oev  8516  oe0  8524  oev2  8525  oneo  8583  nnneo  8656  enpr2d  9051  endisj  9060  map2xp  9149  snnen2o  9239  sdom1  9244  sdom1OLD  9245  rex2dom  9248  1sdom2dom  9249  1sdomOLD  9251  ssttrcl  9712  ttrclselem2  9723  djuexb  9906  djurcl  9908  djurf1o  9910  djuss  9917  djuun  9923  1stinr  9926  2ndinr  9927  pm54.43  9998  dju1dif  10169  djucomen  10174  djuassen  10175  infdju1  10186  pwdju1  10187  nnadju  10194  infmap2  10215  cfsuc  10254  isfin4p1  10312  dcomex  10444  pwcfsdom  10580  cfpwsdom  10581  canthp1lem2  10650  pwxpndom2  10662  indpi  10904  pinq  10924  archnq  10977  sadcf  16396  sadcp1  16398  fnpr2ob  17506  xpsfrnel  17510  xpsle  17527  setcepi  18040  setc2obas  18046  setc2ohom  18047  efgi1  19591  frgpuptinv  19641  dmdprdpr  19921  dprdpr  19922  coe1fval3  21738  00ply1bas  21769  ply1plusgfvi  21771  coe1z  21792  coe1tm  21802  xpstopnlem1  23320  xpstopnlem2  23322  xpsdsval  23894  nofv  27167  noxp1o  27173  noextendlt  27179  bdayfo  27187  nosep1o  27191  nosepdmlem  27193  nolt02o  27205  nogt01o  27206  nosupbnd1lem5  27222  nosupbnd2lem1  27225  noinfno  27228  noinfbday  27230  noinfbnd1  27239  noinfbnd2lem1  27240  noinfbnd2  27241  noetasuplem1  27243  noetasuplem2  27244  noetasuplem4  27246  fply1  32682  gonanegoal  34412  fmlaomn0  34450  gonan0  34452  gonarlem  34454  gonar  34455  fmlasucdisj  34459  satffunlem  34461  satffunlem2lem1  34464  ex-sategoelel12  34487  rankeq1o  35218  bj-pr2val  35991  bj-2upln1upl  35997  pw2f1ocnv  41864  omnord1ex  42142  oege2  42145  oenord1ex  42153  oenord1  42154  oaomoencom  42155  oenassex  42156  cantnfresb  42162  omcl3g  42172  clsk3nimkb  42879  clsk1indlem4  42883  clsk1indlem1  42884  f1omo  47611  f1omoALT  47612  indthinc  47756  indthincALT  47757  prsthinc  47758  prstchom  47781  prstchom2ALT  47783