Theorem 1oex 8307

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

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

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

Syntax hints:   ∈ wcel 2106  Vcvv 3432  ∅c0 4256  {csn 4561  1_oc1o 8290

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-sn 4562  df-pr 4564  df-suc 6272  df-1o 8297

This theorem is referenced by:  1on  8309  2oexOLD  8317  nlim2  8320  oev  8344  oe0  8352  oev2  8353  oneo  8412  nnneo  8485  endisj  8845  map2xp  8934  sdom1  9022  1sdom  9025  snnen2o  9026  ssttrcl  9473  ttrclselem2  9484  djuexb  9667  djurcl  9669  djurf1o  9671  djuss  9678  djuun  9684  1stinr  9687  2ndinr  9688  pm54.43  9759  dju1dif  9928  djucomen  9933  djuassen  9934  infdju1  9945  pwdju1  9946  nnadju  9953  infmap2  9974  cfsuc  10013  isfin4p1  10071  dcomex  10203  pwcfsdom  10339  cfpwsdom  10340  canthp1lem2  10409  pwxpndom2  10421  indpi  10663  pinq  10683  archnq  10736  sadcf  16160  sadcp1  16162  fnpr2ob  17269  xpsfrnel  17273  xpsle  17290  setcepi  17803  setc2obas  17809  setc2ohom  17810  efgi1  19327  frgpuptinv  19377  dmdprdpr  19652  dprdpr  19653  coe1fval3  21379  00ply1bas  21411  ply1plusgfvi  21413  coe1z  21434  coe1tm  21444  xpstopnlem1  22960  xpstopnlem2  22962  xpsdsval  23534  fply1  31667  gonanegoal  33314  fmlaomn0  33352  gonan0  33354  gonarlem  33356  gonar  33357  fmlasucdisj  33361  satffunlem  33363  satffunlem2lem1  33366  ex-sategoelel12  33389  nofv  33860  noxp1o  33866  noextendlt  33872  bdayfo  33880  nosep1o  33884  nosepdmlem  33886  nolt02o  33898  nogt01o  33899  nosupbnd1lem5  33915  nosupbnd2lem1  33918  noinfno  33921  noinfbday  33923  noinfbnd1  33932  noinfbnd2lem1  33933  noinfbnd2  33934  noetasuplem1  33936  noetasuplem2  33937  noetasuplem4  33939  rankeq1o  34473  bj-pr2val  35208  bj-2upln1upl  35214  pw2f1ocnv  40859  clsk3nimkb  41650  clsk1indlem4  41654  clsk1indlem1  41655  f1omo  46188  f1omoALT  46189  indthinc  46333  indthincALT  46334  prsthinc  46335  prstchom  46358  prstchom2ALT  46360