Theorem 1oex 8516

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

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

Step	Hyp	Ref	Expression
1		df1o2 8513	. 2 ⊢ 1o = {∅}
2		snex 5436	. 2 ⊢ {∅} ∈ V
3	1, 2	eqeltri 2837	1 ⊢ 1o ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3480  ∅c0 4333  {csn 4626  1_oc1o 8499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-un 3956  df-nul 4334  df-sn 4627  df-pr 4629  df-suc 6390  df-1o 8506

This theorem is referenced by:  1on  8518  nlim2  8528  oev  8552  oe0  8560  oev2  8561  oneo  8619  nnneo  8693  enpr2d  9089  endisj  9098  map2xp  9187  snnen2o  9273  sdom1  9278  sdom1OLD  9279  rex2dom  9282  1sdom2dom  9283  1sdomOLD  9285  ssttrcl  9755  ttrclselem2  9766  djuexb  9949  djurcl  9951  djurf1o  9953  djuss  9960  djuun  9966  1stinr  9969  2ndinr  9970  pm54.43  10041  dju1dif  10213  djucomen  10218  djuassen  10219  infdju1  10230  pwdju1  10231  nnadju  10238  infmap2  10257  cfsuc  10297  isfin4p1  10355  dcomex  10487  pwcfsdom  10623  cfpwsdom  10624  canthp1lem2  10693  pwxpndom2  10705  indpi  10947  pinq  10967  archnq  11020  sadcf  16490  sadcp1  16492  fnpr2ob  17603  xpsfrnel  17607  xpsle  17624  setcepi  18133  setc2obas  18139  setc2ohom  18140  efgi1  19739  frgpuptinv  19789  dmdprdpr  20069  dprdpr  20070  coe1fval3  22210  00ply1bas  22241  ply1plusgfvi  22243  coe1z  22266  coe1tm  22276  ply1vscl  22388  rhmply1  22390  rhmply1vr1  22391  xpstopnlem1  23817  xpstopnlem2  23819  xpsdsval  24391  nofv  27702  noxp1o  27708  noextendlt  27714  bdayfo  27722  nosep1o  27726  nosepdmlem  27728  nolt02o  27740  nogt01o  27741  nosupbnd1lem5  27757  nosupbnd2lem1  27760  noinfno  27763  noinfbday  27765  noinfbnd1  27774  noinfbnd2lem1  27775  noinfbnd2  27776  noetasuplem1  27778  noetasuplem2  27779  noetasuplem4  27781  fply1  33584  gonanegoal  35357  fmlaomn0  35395  gonan0  35397  gonarlem  35399  gonar  35400  fmlasucdisj  35404  satffunlem  35406  satffunlem2lem1  35409  ex-sategoelel12  35432  rankeq1o  36172  bj-pr2val  37019  bj-2upln1upl  37025  rhmpsr1  42563  pw2f1ocnv  43049  omnord1ex  43317  oege2  43320  oenord1ex  43328  oenord1  43329  oaomoencom  43330  oenassex  43331  cantnfresb  43337  omcl3g  43347  clsk3nimkb  44053  clsk1indlem4  44057  clsk1indlem1  44058  f1omo  48792  f1omoALT  48793  indthinc  49109  indthincALT  49110  prsthinc  49111  prstchom  49166  prstchom2ALT  49168