Theorem 1oex 8409

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

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

Step	Hyp	Ref	Expression
1		df1o2 8406	. 2 ⊢ 1o = {∅}
2		snex 5377	. 2 ⊢ {∅} ∈ V
3	1, 2	eqeltri 2833	1 ⊢ 1o ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3430  ∅c0 4274  {csn 4568  1_oc1o 8392

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-dif 3893  df-un 3895  df-nul 4275  df-sn 4569  df-pr 4571  df-suc 6324  df-1o 8399

This theorem is referenced by:  1on  8411  nlim2  8419  oev  8443  oe0  8451  oev2  8452  oneo  8510  nnneo  8585  enpr2d  8989  endisj  8996  map2xp  9079  snnen2o  9149  sdom1  9154  rex2dom  9157  1sdom2dom  9158  ssttrcl  9630  ttrclselem2  9641  djuexb  9827  djurcl  9829  djurf1o  9831  djuss  9838  djuun  9844  1stinr  9847  2ndinr  9848  pm54.43  9919  dju1dif  10089  djucomen  10094  djuassen  10095  infdju1  10106  pwdju1  10107  nnadju  10114  infmap2  10133  cfsuc  10173  isfin4p1  10231  dcomex  10363  pwcfsdom  10500  cfpwsdom  10501  canthp1lem2  10570  pwxpndom2  10582  indpi  10824  pinq  10844  archnq  10897  sadcf  16416  sadcp1  16418  fnpr2ob  17516  xpsfrnel  17520  xpsle  17537  setcepi  18049  setc2obas  18055  setc2ohom  18056  efgi1  19690  frgpuptinv  19740  dmdprdpr  20020  dprdpr  20021  coe1fval3  22185  00ply1bas  22216  ply1plusgfvi  22218  coe1z  22241  coe1tm  22251  ply1vscl  22362  rhmply1  22364  rhmply1vr1  22365  xpstopnlem1  23787  xpstopnlem2  23789  xpsdsval  24359  nofv  27638  noxp1o  27644  noextendlt  27650  bdayfo  27658  nosep1o  27662  nosepdmlem  27664  nolt02o  27676  nogt01o  27677  nosupbnd1lem5  27693  nosupbnd2lem1  27696  noinfno  27699  noinfbday  27701  noinfbnd1  27710  noinfbnd2lem1  27711  noinfbnd2  27712  noetasuplem1  27714  noetasuplem2  27715  noetasuplem4  27717  fply1  33636  gonanegoal  35553  fmlaomn0  35591  gonan0  35593  gonarlem  35595  gonar  35596  fmlasucdisj  35600  satffunlem  35602  satffunlem2lem1  35605  ex-sategoelel12  35628  rankeq1o  36372  bj-pr2val  37344  bj-2upln1upl  37350  rhmpsr1  43013  pw2f1ocnv  43486  omnord1ex  43753  oege2  43756  oenord1ex  43764  oenord1  43765  oaomoencom  43766  oenassex  43767  cantnfresb  43773  omcl3g  43783  clsk3nimkb  44488  clsk1indlem4  44492  clsk1indlem1  44493  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