Theorem 1oex 8377

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

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

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

Syntax hints:   ∈ wcel 2105  Vcvv 3441  ∅c0 4269  {csn 4573  1_oc1o 8360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707  ax-sep 5243  ax-nul 5250  ax-pr 5372

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3443  df-dif 3901  df-un 3903  df-nul 4270  df-sn 4574  df-pr 4576  df-suc 6308  df-1o 8367

This theorem is referenced by:  1on  8379  2oexOLD  8388  nlim2  8391  oev  8415  oe0  8423  oev2  8424  oneo  8483  nnneo  8556  enpr2d  8914  endisj  8923  map2xp  9012  snnen2o  9102  sdom1  9107  sdom1OLD  9108  rex2dom  9111  1sdom2dom  9112  1sdomOLD  9114  ssttrcl  9572  ttrclselem2  9583  djuexb  9766  djurcl  9768  djurf1o  9770  djuss  9777  djuun  9783  1stinr  9786  2ndinr  9787  pm54.43  9858  dju1dif  10029  djucomen  10034  djuassen  10035  infdju1  10046  pwdju1  10047  nnadju  10054  infmap2  10075  cfsuc  10114  isfin4p1  10172  dcomex  10304  pwcfsdom  10440  cfpwsdom  10441  canthp1lem2  10510  pwxpndom2  10522  indpi  10764  pinq  10784  archnq  10837  sadcf  16259  sadcp1  16261  fnpr2ob  17366  xpsfrnel  17370  xpsle  17387  setcepi  17900  setc2obas  17906  setc2ohom  17907  efgi1  19422  frgpuptinv  19472  dmdprdpr  19747  dprdpr  19748  coe1fval3  21485  00ply1bas  21517  ply1plusgfvi  21519  coe1z  21540  coe1tm  21550  xpstopnlem1  23066  xpstopnlem2  23068  xpsdsval  23640  nofv  26911  noxp1o  26917  noextendlt  26923  bdayfo  26931  nosep1o  26935  nosepdmlem  26937  nolt02o  26949  nogt01o  26950  nosupbnd1lem5  26966  nosupbnd2lem1  26969  noinfno  26972  noinfbday  26974  noinfbnd1  26983  noinfbnd2lem1  26984  noinfbnd2  26985  noetasuplem1  26987  noetasuplem2  26988  noetasuplem4  26990  fply1  31964  gonanegoal  33613  fmlaomn0  33651  gonan0  33653  gonarlem  33655  gonar  33656  fmlasucdisj  33660  satffunlem  33662  satffunlem2lem1  33665  ex-sategoelel12  33688  rankeq1o  34569  bj-pr2val  35302  bj-2upln1upl  35308  pw2f1ocnv  41122  omcl3g  41319  clsk3nimkb  41971  clsk1indlem4  41975  clsk1indlem1  41976  f1omo  46539  f1omoALT  46540  indthinc  46684  indthincALT  46685  prsthinc  46686  prstchom  46709  prstchom2ALT  46711