Theorem 1oex 8280

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

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

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

Syntax hints:   ∈ wcel 2108  Vcvv 3422  ∅c0 4253  {csn 4558  1_oc1o 8260

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-sn 4559  df-pr 4561  df-suc 6257  df-1o 8267

This theorem is referenced by:  2oexOLD  8285  oev  8306  oe0  8314  oev2  8315  oneo  8374  nnneo  8445  endisj  8799  map2xp  8883  sdom1  8952  1sdom  8955  djuexb  9598  djurcl  9600  djurf1o  9602  djuss  9609  djuun  9615  1stinr  9618  2ndinr  9619  pm54.43  9690  dju1dif  9859  djucomen  9864  djuassen  9865  infdju1  9876  pwdju1  9877  nnadju  9884  infmap2  9905  cfsuc  9944  isfin4p1  10002  dcomex  10134  pwcfsdom  10270  cfpwsdom  10271  canthp1lem2  10340  pwxpndom2  10352  indpi  10594  pinq  10614  archnq  10667  sadcf  16088  sadcp1  16090  fnpr2ob  17186  xpsfrnel  17190  xpsle  17207  setcepi  17719  setc2obas  17725  setc2ohom  17726  efgi1  19242  frgpuptinv  19292  dmdprdpr  19567  dprdpr  19568  coe1fval3  21289  00ply1bas  21321  ply1plusgfvi  21323  coe1z  21344  coe1tm  21354  xpstopnlem1  22868  xpstopnlem2  22870  xpsdsval  23442  fply1  31569  gonanegoal  33214  fmlaomn0  33252  gonan0  33254  gonarlem  33256  gonar  33257  fmlasucdisj  33261  satffunlem  33263  satffunlem2lem1  33266  ex-sategoelel12  33289  ssttrcl  33701  ttrclselem2  33712  nofv  33787  noxp1o  33793  noextendlt  33799  bdayfo  33807  nosep1o  33811  nosepdmlem  33813  nolt02o  33825  nogt01o  33826  nosupbnd1lem5  33842  nosupbnd2lem1  33845  noinfno  33848  noinfbday  33850  noinfbnd1  33859  noinfbnd2lem1  33860  noinfbnd2  33861  noetasuplem1  33863  noetasuplem2  33864  noetasuplem4  33866  rankeq1o  34400  bj-pr2val  35135  bj-2upln1upl  35141  pw2f1ocnv  40775  clsk3nimkb  41539  clsk1indlem4  41543  clsk1indlem1  41544  f1omo  46076  f1omoALT  46077  indthinc  46221  indthincALT  46222  prsthinc  46223  prstchom  46244  prstchom2ALT  46246