Theorem 1oex 8479

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

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

Step	Hyp	Ref	Expression
1		df1o2 8476	. 2 ⊢ 1o = {∅}
2		snex 5397	. 2 ⊢ {∅} ∈ V
3	1, 2	eqeltri 2857	1 ⊢ 1o ∈ V

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451  ∅c0 4279  {csn 4584  1_oc1o 8462

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-dif 3902  df-un 3904  df-nul 4280  df-sn 4585  df-pr 4587  df-suc 6367  df-1o 8469

This theorem is used by:  1oelpr  8480  1on  8482  nlim2  8491  oev  8515  oe0  8523  oev2  8524  oneo  8582  nnneo  8657  enpr2d  9069  endisj  9076  map2xp  9159  snnen2o  9229  sdom1  9234  rex2dom  9237  1sdom2dom  9238  ssttrcl  9709  ttrclselem2  9720  djuexb  9983  djurcl  9985  djurf1o  9987  djuun  10000  1stinr  10003  2ndinr  10004  pm54.43  10075  dju1dif  10244  djucomen  10249  djuassen  10250  infdju1  10261  pwdju1  10262  nnadju  10269  infmap2  10288  cfsuc  10328  isfin4p1  10386  dcomex  10518  pwcfsdom  10661  cfpwsdom  10662  canthp1lem2  10731  pwxpndom2  10743  indpi  10985  pinq  11005  archnq  11058  sadcp1  16618  fnpr2ob  17723  xpsfrnel  17727  xpsle  17744  degenmgmopdm  19127  degenmgmnfn  19129  degenmgm  19130  degenmgm2opdm  19131  degenmgm2nfun  19132  degenmgm2  19133  dmdprdpr  20258  coe1fval3  22519  00ply1bas  22550  ply1plusgfvi  22552  coe1z  22575  coe1tm  22585  ply1vscl  22692  rhmply1  22694  rhmply1vr1  22695  xpsdsval  24693  nofv  28007  noxp1o  28013  noextendlt  28019  bdayfo  28027  nosep1o  28031  nosepdmlem  28033  nolt02o  28045  nogt01o  28046  nosupbnd1lem5  28062  nosupbnd2lem1  28065  noinfno  28068  noinfbday  28070  noinfbnd1  28079  noinfbnd2lem1  28080  noinfbnd2  28081  noetasuplem1  28083  noetasuplem2  28084  noetasuplem4  28086  fply1  34083  selvply1rhmlema  34143  selvply1rhmlemb  34144  selvply1rhmlem1  34145  selvply1rhmlem2  34146  selvply1rhm0  34151  gonanegoal  36096  fmlaomn0  36134  gonan0  36136  gonarlem  36138  gonar  36139  fmlasucdisj  36143  satffunlem  36145  satffunlem2lem1  36148  ex-sategoelel12  36171  rankeq1o  36912  bj-pr2val  37911  bj-2upln1upl  37917  rhmpsr1  43592  pw2f1ocnv  44023  oenord1ex  44301  oenord1  44302  cantnfresb  44310  clsk3nimkb  45025  clsk1indlem4  45029  f1omo  49970  f1omoOLD  49971  f1omoALT  49972  nelsubc3  50148  indthinc  50539  indthincALT  50540  prsthinc  50541  setc1obas  50569  setc1ohomfval  50570  setc1oid  50572  isinito2lem  50575  isinito3  50577  prstchom  50639  prstchom2ALT  50641  setc1onsubc  50679  cnelsubc  50681