Theorem 1oex 8524

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

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

Step	Hyp	Ref	Expression
1		df1o2 8521	. 2 ⊢ 1o = {∅}
2		snex 5404	. 2 ⊢ {∅} ∈ V
3	1, 2	eqeltri 2860	1 ⊢ 1o ∈ V

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454  ∅c0 4281  {csn 4588  1_oc1o 8507

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-dif 4050  df-un 4154  df-nul 4282  df-sn 4589  df-pr 4591  df-suc 6394  df-1o 8514

This theorem is used by:  1oelpr  8525  1on  8527  nlim2  8536  oev  8560  oe0  8568  oev2  8569  oneo  8627  nnneo  8702  enpr2d  9114  endisj  9121  map2xp  9204  snnen2o  9274  sdom1  9279  rex2dom  9282  1sdom2dom  9283  ssttrcl  9753  ttrclselem2  9764  djuexb  10027  djurcl  10029  djurf1o  10031  djuun  10044  1stinr  10047  2ndinr  10048  pm54.43  10121  dju1dif  10290  djucomen  10295  djuassen  10296  infdju1  10307  pwdju1  10308  nnadju  10315  infmap2  10334  cfsuc  10374  isfin4p1  10432  dcomex  10564  pwcfsdom  10707  cfpwsdom  10708  canthp1lem2  10777  pwxpndom2  10789  indpi  11031  pinq  11051  archnq  11104  sadcp1  16669  fnpr2ob  17780  xpsfrnel  17784  xpsle  17801  degenmgmopdm  19184  degenmgmnfn  19186  degenmgm  19187  degenmgm2opdm  19188  degenmgm2nfun  19189  degenmgm2  19190  dmdprdpr  20316  coe1fval3  22581  00ply1bas  22612  ply1plusgfvi  22614  coe1z  22637  coe1tm  22647  ply1vscl  22754  rhmply1  22756  rhmply1vr1  22757  xpsdsval  24755  nofv  28071  noxp1o  28077  noextendlt  28083  bdayfo  28091  nosep1o  28095  nosepdmlem  28097  nolt02o  28109  nogt01o  28110  nosupbnd1lem5  28126  nosupbnd2lem1  28129  noinfno  28132  noinfbday  28134  noinfbnd1  28143  noinfbnd2lem1  28144  noinfbnd2  28145  noetasuplem1  28147  noetasuplem2  28148  noetasuplem4  28150  fply1  34193  selvply1rhmlema  34261  selvply1rhmlemb  34262  selvply1rhmlem1  34263  selvply1rhmlem2  34264  selvply1rhm0  34269  gonanegoal  36325  fmlaomn0  36363  gonan0  36365  gonarlem  36367  gonar  36368  fmlasucdisj  36372  satffunlem  36374  satffunlem2lem1  36377  ex-sategoelel12  36400  rankeq1o  37147  bj-pr2val  38146  bj-2upln1upl  38152  rhmpsr1  43878  pw2f1ocnv  44310  oenord1ex  44578  oenord1  44579  cantnfresb  44587  clsk3nimkb  45301  clsk1indlem4  45305  f1omo  50338  f1omoOLD  50339  f1omoALT  50340  nelsubc3  50516  indthinc  50928  indthincALT  50929  prsthinc  50930  setc1obas  50958  setc1ohomfval  50959  setc1oid  50961  isinito2lem  50964  isinito3  50966  prstchom  51031  prstchom2ALT  51033  setc1onsubc  51071  cnelsubc  51073  parswapval  51107