Theorem 1oex 8465

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

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

Step	Hyp	Ref	Expression
1		df1o2 8462	. 2 ⊢ 1o = {∅}
2		snex 5404	. 2 ⊢ {∅} ∈ V
3	1, 2	eqeltri 2856	1 ⊢ 1o ∈ V

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3450  ∅c0 4279  {csn 4584  1_oc1o 8448

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 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 3902  df-un 3904  df-nul 4280  df-sn 4585  df-pr 4587  df-suc 6363  df-1o 8455

This theorem is used by:  1oelpr  8466  1on  8468  nlim2  8477  oev  8501  oe0  8509  oev2  8510  oneo  8568  nnneo  8643  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  10592  cfpwsdom  10593  canthp1lem2  10662  pwxpndom2  10674  indpi  10916  pinq  10936  archnq  10989  sadcp1  16545  fnpr2ob  17644  xpsfrnel  17648  xpsle  17665  degenmgmopdm  19047  degenmgmnfn  19049  degenmgm  19050  degenmgm2opdm  19051  degenmgm2nfun  19052  degenmgm2  19053  dmdprdpr  20178  coe1fval3  22433  00ply1bas  22464  ply1plusgfvi  22466  coe1z  22489  coe1tm  22499  ply1vscl  22606  rhmply1  22608  rhmply1vr1  22609  xpsdsval  24607  nofv  27893  noxp1o  27899  noextendlt  27905  bdayfo  27913  nosep1o  27917  nosepdmlem  27919  nolt02o  27931  nogt01o  27932  nosupbnd1lem5  27948  nosupbnd2lem1  27951  noinfno  27954  noinfbday  27956  noinfbnd1  27965  noinfbnd2lem1  27966  noinfbnd2  27967  noetasuplem1  27969  noetasuplem2  27970  noetasuplem4  27972  fply1  33968  selvply1rhmlema  34028  selvply1rhmlemb  34029  selvply1rhmlem1  34030  selvply1rhmlem2  34031  selvply1rhm0  34036  gonanegoal  35931  fmlaomn0  35969  gonan0  35971  gonarlem  35973  gonar  35974  fmlasucdisj  35978  satffunlem  35980  satffunlem2lem1  35983  ex-sategoelel12  36006  rankeq1o  36751  bj-pr2val  37762  bj-2upln1upl  37768  rhmpsr1  43430  pw2f1ocnv  43878  oenord1ex  44156  oenord1  44157  cantnfresb  44165  clsk3nimkb  44880  clsk1indlem4  44884  f1omo  49819  f1omoOLD  49820  f1omoALT  49821  nelsubc3  49997  indthinc  50388  indthincALT  50389  prsthinc  50390  setc1obas  50418  setc1ohomfval  50419  setc1oid  50421  isinito2lem  50424  isinito3  50426  prstchom  50488  prstchom2ALT  50490  setc1onsubc  50528  cnelsubc  50530