Theorem 1oex 8493

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

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

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

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450  ∅c0 4277  {csn 4584  1_oc1o 8476

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 4046  df-un 4150  df-nul 4278  df-sn 4585  df-pr 4587  df-suc 6371  df-1o 8483

This theorem is used by:  1oelpr  8494  1on  8496  nlim2  8505  oev  8529  oe0  8537  oev2  8538  oneo  8596  nnneo  8671  enpr2d  9083  endisj  9090  map2xp  9173  snnen2o  9243  sdom1  9248  rex2dom  9251  1sdom2dom  9252  ssttrcl  9723  ttrclselem2  9734  djuexb  9997  djurcl  9999  djurf1o  10001  djuun  10014  1stinr  10017  2ndinr  10018  pm54.43  10089  dju1dif  10258  djucomen  10263  djuassen  10264  infdju1  10275  pwdju1  10276  nnadju  10283  infmap2  10302  cfsuc  10342  isfin4p1  10400  dcomex  10532  pwcfsdom  10675  cfpwsdom  10676  canthp1lem2  10745  pwxpndom2  10757  indpi  10999  pinq  11019  archnq  11072  sadcp1  16634  fnpr2ob  17739  xpsfrnel  17743  xpsle  17760  degenmgmopdm  19143  degenmgmnfn  19145  degenmgm  19146  degenmgm2opdm  19147  degenmgm2nfun  19148  degenmgm2  19149  dmdprdpr  20274  coe1fval3  22535  00ply1bas  22566  ply1plusgfvi  22568  coe1z  22591  coe1tm  22601  ply1vscl  22708  rhmply1  22710  rhmply1vr1  22711  xpsdsval  24709  nofv  28023  noxp1o  28029  noextendlt  28035  bdayfo  28043  nosep1o  28047  nosepdmlem  28049  nolt02o  28061  nogt01o  28062  nosupbnd1lem5  28078  nosupbnd2lem1  28081  noinfno  28084  noinfbday  28086  noinfbnd1  28095  noinfbnd2lem1  28096  noinfbnd2  28097  noetasuplem1  28099  noetasuplem2  28100  noetasuplem4  28102  fply1  34140  selvply1rhmlema  34200  selvply1rhmlemb  34201  selvply1rhmlem1  34202  selvply1rhmlem2  34203  selvply1rhm0  34208  gonanegoal  36207  fmlaomn0  36245  gonan0  36247  gonarlem  36249  gonar  36250  fmlasucdisj  36254  satffunlem  36256  satffunlem2lem1  36259  ex-sategoelel12  36282  rankeq1o  37028  bj-pr2val  38027  bj-2upln1upl  38033  rhmpsr1  43721  pw2f1ocnv  44153  oenord1ex  44426  oenord1  44427  cantnfresb  44435  clsk3nimkb  45149  clsk1indlem4  45153  f1omo  50115  f1omoOLD  50116  f1omoALT  50117  nelsubc3  50293  indthinc  50705  indthincALT  50706  prsthinc  50707  setc1obas  50735  setc1ohomfval  50736  setc1oid  50738  isinito2lem  50741  isinito3  50743  prstchom  50808  prstchom2ALT  50810  setc1onsubc  50848  cnelsubc  50850  parswapval  50884