Theorem 1oex 8395

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

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

Step	Hyp	Ref	Expression
1		df1o2 8392	. 2 ⊢ 1o = {∅}
2		snex 5372	. 2 ⊢ {∅} ∈ V
3	1, 2	eqeltri 2827	1 ⊢ 1o ∈ V

Syntax hints:   ∈ wcel 2111  Vcvv 3436  ∅c0 4280  {csn 4573  1_oc1o 8378

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 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3900  df-un 3902  df-nul 4281  df-sn 4574  df-pr 4576  df-suc 6312  df-1o 8385

This theorem is referenced by:  1on  8397  nlim2  8405  oev  8429  oe0  8437  oev2  8438  oneo  8496  nnneo  8570  enpr2d  8970  endisj  8977  map2xp  9060  snnen2o  9129  sdom1  9134  rex2dom  9137  1sdom2dom  9138  ssttrcl  9605  ttrclselem2  9616  djuexb  9802  djurcl  9804  djurf1o  9806  djuss  9813  djuun  9819  1stinr  9822  2ndinr  9823  pm54.43  9894  dju1dif  10064  djucomen  10069  djuassen  10070  infdju1  10081  pwdju1  10082  nnadju  10089  infmap2  10108  cfsuc  10148  isfin4p1  10206  dcomex  10338  pwcfsdom  10474  cfpwsdom  10475  canthp1lem2  10544  pwxpndom2  10556  indpi  10798  pinq  10818  archnq  10871  sadcf  16364  sadcp1  16366  fnpr2ob  17462  xpsfrnel  17466  xpsle  17483  setcepi  17995  setc2obas  18001  setc2ohom  18002  efgi1  19633  frgpuptinv  19683  dmdprdpr  19963  dprdpr  19964  coe1fval3  22121  00ply1bas  22152  ply1plusgfvi  22154  coe1z  22177  coe1tm  22187  ply1vscl  22299  rhmply1  22301  rhmply1vr1  22302  xpstopnlem1  23724  xpstopnlem2  23726  xpsdsval  24296  nofv  27596  noxp1o  27602  noextendlt  27608  bdayfo  27616  nosep1o  27620  nosepdmlem  27622  nolt02o  27634  nogt01o  27635  nosupbnd1lem5  27651  nosupbnd2lem1  27654  noinfno  27657  noinfbday  27659  noinfbnd1  27668  noinfbnd2lem1  27669  noinfbnd2  27670  noetasuplem1  27672  noetasuplem2  27673  noetasuplem4  27675  fply1  33521  gonanegoal  35396  fmlaomn0  35434  gonan0  35436  gonarlem  35438  gonar  35439  fmlasucdisj  35443  satffunlem  35445  satffunlem2lem1  35448  ex-sategoelel12  35471  rankeq1o  36213  bj-pr2val  37060  bj-2upln1upl  37066  rhmpsr1  42594  pw2f1ocnv  43078  omnord1ex  43345  oege2  43348  oenord1ex  43356  oenord1  43357  oaomoencom  43358  oenassex  43359  cantnfresb  43365  omcl3g  43375  clsk3nimkb  44081  clsk1indlem4  44085  clsk1indlem1  44086  f1omo  48932  f1omoOLD  48933  f1omoALT  48934  nelsubc3  49111  indthinc  49502  indthincALT  49503  prsthinc  49504  setc1obas  49532  setc1ohomfval  49533  setc1oid  49535  isinito2lem  49538  isinito3  49540  prstchom  49602  prstchom2ALT  49604  setc1onsubc  49642  cnelsubc  49644