Theorem 1oex 8407

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 2184, ax-un 7680. (Revised by Zhi Wang, 19-Sep-2024.)

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

Step	Hyp	Ref	Expression
1		df1o2 8404	. 2 ⊢ 1o = {∅}
2		snex 5381	. 2 ⊢ {∅} ∈ V
3	1, 2	eqeltri 2832	1 ⊢ 1o ∈ V

Syntax hints:   ∈ wcel 2113  Vcvv 3440  ∅c0 4285  {csn 4580  1_oc1o 8390

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 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-un 3906  df-nul 4286  df-sn 4581  df-pr 4583  df-suc 6323  df-1o 8397

This theorem is referenced by:  1on  8409  nlim2  8417  oev  8441  oe0  8449  oev2  8450  oneo  8508  nnneo  8583  enpr2d  8985  endisj  8992  map2xp  9075  snnen2o  9145  sdom1  9150  rex2dom  9153  1sdom2dom  9154  ssttrcl  9624  ttrclselem2  9635  djuexb  9821  djurcl  9823  djurf1o  9825  djuss  9832  djuun  9838  1stinr  9841  2ndinr  9842  pm54.43  9913  dju1dif  10083  djucomen  10088  djuassen  10089  infdju1  10100  pwdju1  10101  nnadju  10108  infmap2  10127  cfsuc  10167  isfin4p1  10225  dcomex  10357  pwcfsdom  10494  cfpwsdom  10495  canthp1lem2  10564  pwxpndom2  10576  indpi  10818  pinq  10838  archnq  10891  sadcf  16380  sadcp1  16382  fnpr2ob  17479  xpsfrnel  17483  xpsle  17500  setcepi  18012  setc2obas  18018  setc2ohom  18019  efgi1  19650  frgpuptinv  19700  dmdprdpr  19980  dprdpr  19981  coe1fval3  22149  00ply1bas  22180  ply1plusgfvi  22182  coe1z  22205  coe1tm  22215  ply1vscl  22328  rhmply1  22330  rhmply1vr1  22331  xpstopnlem1  23753  xpstopnlem2  23755  xpsdsval  24325  nofv  27625  noxp1o  27631  noextendlt  27637  bdayfo  27645  nosep1o  27649  nosepdmlem  27651  nolt02o  27663  nogt01o  27664  nosupbnd1lem5  27680  nosupbnd2lem1  27683  noinfno  27686  noinfbday  27688  noinfbnd1  27697  noinfbnd2lem1  27698  noinfbnd2  27699  noetasuplem1  27701  noetasuplem2  27702  noetasuplem4  27704  fply1  33639  gonanegoal  35546  fmlaomn0  35584  gonan0  35586  gonarlem  35588  gonar  35589  fmlasucdisj  35593  satffunlem  35595  satffunlem2lem1  35598  ex-sategoelel12  35621  rankeq1o  36365  bj-pr2val  37219  bj-2upln1upl  37225  rhmpsr1  42806  pw2f1ocnv  43279  omnord1ex  43546  oege2  43549  oenord1ex  43557  oenord1  43558  oaomoencom  43559  oenassex  43560  cantnfresb  43566  omcl3g  43576  clsk3nimkb  44281  clsk1indlem4  44285  clsk1indlem1  44286  f1omo  49138  f1omoOLD  49139  f1omoALT  49140  nelsubc3  49316  indthinc  49707  indthincALT  49708  prsthinc  49709  setc1obas  49737  setc1ohomfval  49738  setc1oid  49740  isinito2lem  49743  isinito3  49745  prstchom  49807  prstchom2ALT  49809  setc1onsubc  49847  cnelsubc  49849