Theorem 1oex 8476

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

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

Step	Hyp	Ref	Expression
1		df1o2 8473	. 2 ⊢ 1o = {∅}
2		snex 5432	. 2 ⊢ {∅} ∈ V
3	1, 2	eqeltri 2830	1 ⊢ 1o ∈ V

Syntax hints:   ∈ wcel 2107  Vcvv 3475  ∅c0 4323  {csn 4629  1_oc1o 8459

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952  df-un 3954  df-nul 4324  df-sn 4630  df-pr 4632  df-suc 6371  df-1o 8466

This theorem is referenced by:  1on  8478  2oexOLD  8487  nlim2  8490  oev  8514  oe0  8522  oev2  8523  oneo  8581  nnneo  8654  enpr2d  9049  endisj  9058  map2xp  9147  snnen2o  9237  sdom1  9242  sdom1OLD  9243  rex2dom  9246  1sdom2dom  9247  1sdomOLD  9249  ssttrcl  9710  ttrclselem2  9721  djuexb  9904  djurcl  9906  djurf1o  9908  djuss  9915  djuun  9921  1stinr  9924  2ndinr  9925  pm54.43  9996  dju1dif  10167  djucomen  10172  djuassen  10173  infdju1  10184  pwdju1  10185  nnadju  10192  infmap2  10213  cfsuc  10252  isfin4p1  10310  dcomex  10442  pwcfsdom  10578  cfpwsdom  10579  canthp1lem2  10648  pwxpndom2  10660  indpi  10902  pinq  10922  archnq  10975  sadcf  16394  sadcp1  16396  fnpr2ob  17504  xpsfrnel  17508  xpsle  17525  setcepi  18038  setc2obas  18044  setc2ohom  18045  efgi1  19589  frgpuptinv  19639  dmdprdpr  19919  dprdpr  19920  coe1fval3  21732  00ply1bas  21762  ply1plusgfvi  21764  coe1z  21785  coe1tm  21795  xpstopnlem1  23313  xpstopnlem2  23315  xpsdsval  23887  nofv  27160  noxp1o  27166  noextendlt  27172  bdayfo  27180  nosep1o  27184  nosepdmlem  27186  nolt02o  27198  nogt01o  27199  nosupbnd1lem5  27215  nosupbnd2lem1  27218  noinfno  27221  noinfbday  27223  noinfbnd1  27232  noinfbnd2lem1  27233  noinfbnd2  27234  noetasuplem1  27236  noetasuplem2  27237  noetasuplem4  27239  fply1  32637  gonanegoal  34343  fmlaomn0  34381  gonan0  34383  gonarlem  34385  gonar  34386  fmlasucdisj  34390  satffunlem  34392  satffunlem2lem1  34395  ex-sategoelel12  34418  rankeq1o  35143  bj-pr2val  35899  bj-2upln1upl  35905  pw2f1ocnv  41776  omnord1ex  42054  oege2  42057  oenord1ex  42065  oenord1  42066  oaomoencom  42067  oenassex  42068  cantnfresb  42074  omcl3g  42084  clsk3nimkb  42791  clsk1indlem4  42795  clsk1indlem1  42796  f1omo  47527  f1omoALT  47528  indthinc  47672  indthincALT  47673  prsthinc  47674  prstchom  47697  prstchom2ALT  47699