Theorem 1oex 8472

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

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

Step	Hyp	Ref	Expression
1		df1o2 8469	. 2 ⊢ 1o = {∅}
2		snex 5415	. 2 ⊢ {∅} ∈ V
3	1, 2	eqeltri 2862	1 ⊢ 1o ∈ V

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3458  ∅c0 4289  {csn 4594  1_oc1o 8455

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-dif 3911  df-un 3913  df-nul 4290  df-sn 4595  df-pr 4597  df-suc 6373  df-1o 8462

This theorem is used by:  1oelpr  8473  1on  8475  nlim2  8484  oev  8508  oe0  8516  oev2  8517  oneo  8575  nnneo  8650  enpr2d  9055  endisj  9062  map2xp  9145  snnen2o  9215  sdom1  9220  rex2dom  9223  1sdom2dom  9224  ssttrcl  9694  ttrclselem2  9705  djuexb  9914  djurcl  9916  djurf1o  9918  djuun  9931  1stinr  9934  2ndinr  9935  pm54.43  10006  dju1dif  10175  djucomen  10180  djuassen  10181  infdju1  10192  pwdju1  10193  nnadju  10200  infmap2  10219  cfsuc  10259  isfin4p1  10317  dcomex  10449  pwcfsdom  10586  cfpwsdom  10587  canthp1lem2  10656  pwxpndom2  10668  indpi  10910  pinq  10930  archnq  10983  sadcp1  16538  fnpr2ob  17637  xpsfrnel  17641  xpsle  17658  dmdprdpr  20152  coe1fval3  22405  00ply1bas  22436  ply1plusgfvi  22438  coe1z  22461  coe1tm  22471  ply1vscl  22578  rhmply1  22580  rhmply1vr1  22581  xpsdsval  24575  nofv  27858  noxp1o  27864  noextendlt  27870  bdayfo  27878  nosep1o  27882  nosepdmlem  27884  nolt02o  27896  nogt01o  27897  nosupbnd1lem5  27913  nosupbnd2lem1  27916  noinfno  27919  noinfbday  27921  noinfbnd1  27930  noinfbnd2lem1  27931  noinfbnd2  27932  noetasuplem1  27934  noetasuplem2  27935  noetasuplem4  27937  fply1  33879  selvply1rhmlema  33939  selvply1rhmlemb  33940  selvply1rhmlem1  33941  selvply1rhmlem2  33942  selvply1rhmlem4  33944  selvply1rhm0  33947  gonanegoal  35864  fmlaomn0  35902  gonan0  35904  gonarlem  35906  gonar  35907  fmlasucdisj  35911  satffunlem  35913  satffunlem2lem1  35916  ex-sategoelel12  35939  rankeq1o  36683  bj-pr2val  37694  bj-2upln1upl  37700  rhmpsr1  43356  pw2f1ocnv  43804  oenord1ex  44082  oenord1  44083  cantnfresb  44091  clsk3nimkb  44806  clsk1indlem4  44810  f1omo  49711  f1omoOLD  49712  f1omoALT  49713  nelsubc3  49889  indthinc  50280  indthincALT  50281  prsthinc  50282  setc1obas  50310  setc1ohomfval  50311  setc1oid  50313  isinito2lem  50316  isinito3  50318  prstchom  50380  prstchom2ALT  50382  setc1onsubc  50420  cnelsubc  50422