Theorem 1oex 8405

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

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

Step	Hyp	Ref	Expression
1		df1o2 8402	. 2 ⊢ 1o = {∅}
2		snex 5368	. 2 ⊢ {∅} ∈ V
3	1, 2	eqeltri 2835	1 ⊢ 1o ∈ V

Syntax hints:   ∈ wcel 2119  Vcvv 3431  ∅c0 4261  {csn 4555  1_oc1o 8388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-dif 3886  df-un 3888  df-nul 4262  df-sn 4556  df-pr 4558  df-suc 6316  df-1o 8395

This theorem is referenced by:  1on  8407  nlim2  8415  oev  8439  oe0  8447  oev2  8448  oneo  8506  nnneo  8581  enpr2d  8985  endisj  8992  map2xp  9075  snnen2o  9145  sdom1  9150  rex2dom  9153  1sdom2dom  9154  ssttrcl  9627  ttrclselem2  9638  djuexb  9824  djurcl  9826  djurf1o  9828  djuss  9835  djuun  9841  1stinr  9844  2ndinr  9845  pm54.43  9916  dju1dif  10086  djucomen  10091  djuassen  10092  infdju1  10103  pwdju1  10104  nnadju  10111  infmap2  10130  cfsuc  10170  isfin4p1  10228  dcomex  10360  pwcfsdom  10497  cfpwsdom  10498  canthp1lem2  10567  pwxpndom2  10579  indpi  10821  pinq  10841  archnq  10894  sadcf  16413  sadcp1  16415  fnpr2ob  17513  xpsfrnel  17517  xpsle  17534  setcepi  18046  setc2obas  18052  setc2ohom  18053  efgi1  19687  frgpuptinv  19737  dmdprdpr  20017  dprdpr  20018  coe1fval3  22193  00ply1bas  22224  ply1plusgfvi  22226  coe1z  22249  coe1tm  22259  ply1vscl  22367  rhmply1  22369  rhmply1vr1  22370  xpstopnlem1  23792  xpstopnlem2  23794  xpsdsval  24364  nofv  27639  noxp1o  27645  noextendlt  27651  bdayfo  27659  nosep1o  27663  nosepdmlem  27665  nolt02o  27677  nogt01o  27678  nosupbnd1lem5  27694  nosupbnd2lem1  27697  noinfno  27700  noinfbday  27702  noinfbnd1  27711  noinfbnd2lem1  27712  noinfbnd2  27713  noetasuplem1  27715  noetasuplem2  27716  noetasuplem4  27718  fply1  33641  selvply1rhmlema  33702  selvply1rhmlemb  33703  selvply1rhmlem1  33704  selvply1rhmlem2  33705  selvply1rhmlem4  33707  selvply1rhm0  33710  gonanegoal  35580  fmlaomn0  35618  gonan0  35620  gonarlem  35622  gonar  35623  fmlasucdisj  35627  satffunlem  35629  satffunlem2lem1  35632  ex-sategoelel12  35655  rankeq1o  36399  bj-pr2val  37371  bj-2upln1upl  37377  rhmpsr1  43034  pw2f1ocnv  43482  omnord1ex  43749  oege2  43752  oenord1ex  43760  oenord1  43761  oaomoencom  43762  oenassex  43763  cantnfresb  43769  omcl3g  43779  clsk3nimkb  44484  clsk1indlem4  44488  clsk1indlem1  44489  f1omo  49383  f1omoOLD  49384  f1omoALT  49385  nelsubc3  49561  indthinc  49952  indthincALT  49953  prsthinc  49954  setc1obas  49982  setc1ohomfval  49983  setc1oid  49985  isinito2lem  49988  isinito3  49990  prstchom  50052  prstchom2ALT  50054  setc1onsubc  50092  cnelsubc  50094