Theorem 1oex 8459

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

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

Step	Hyp	Ref	Expression
1		df1o2 8456	. 2 ⊢ 1o = {∅}
2		snex 5410	. 2 ⊢ {∅} ∈ V
3	1, 2	eqeltri 2859	1 ⊢ 1o ∈ V

Syntax hints:   ∈ wcel 2143  Vcvv 3455  ∅c0 4286  {csn 4589  1_oc1o 8442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3908  df-un 3910  df-nul 4287  df-sn 4590  df-pr 4592  df-suc 6366  df-1o 8449

This theorem is referenced by:  1oelpr  8460  1on  8462  nlim2  8471  oev  8495  oe0  8503  oev2  8504  oneo  8562  nnneo  8637  enpr2d  9041  endisj  9048  map2xp  9131  snnen2o  9201  sdom1  9206  rex2dom  9209  1sdom2dom  9210  ssttrcl  9680  ttrclselem2  9691  djuexb  9891  djurcl  9893  djurf1o  9895  djuun  9908  1stinr  9911  2ndinr  9912  pm54.43  9983  dju1dif  10152  djucomen  10157  djuassen  10158  infdju1  10169  pwdju1  10170  nnadju  10177  infmap2  10196  cfsuc  10236  isfin4p1  10294  dcomex  10426  pwcfsdom  10563  cfpwsdom  10564  canthp1lem2  10633  pwxpndom2  10645  indpi  10887  pinq  10907  archnq  10960  sadcp1  16508  fnpr2ob  17607  xpsfrnel  17611  xpsle  17628  dmdprdpr  20116  coe1fval3  22368  00ply1bas  22399  ply1plusgfvi  22401  coe1z  22424  coe1tm  22434  ply1vscl  22541  rhmply1  22543  rhmply1vr1  22544  xpsdsval  24538  nofv  27821  noxp1o  27827  noextendlt  27833  bdayfo  27841  nosep1o  27845  nosepdmlem  27847  nolt02o  27859  nogt01o  27860  nosupbnd1lem5  27876  nosupbnd2lem1  27879  noinfno  27882  noinfbday  27884  noinfbnd1  27893  noinfbnd2lem1  27894  noinfbnd2  27895  noetasuplem1  27897  noetasuplem2  27898  noetasuplem4  27900  fply1  33848  selvply1rhmlema  33908  selvply1rhmlemb  33909  selvply1rhmlem1  33910  selvply1rhmlem2  33911  selvply1rhmlem4  33913  selvply1rhm0  33916  gonanegoal  35844  fmlaomn0  35882  gonan0  35884  gonarlem  35886  gonar  35887  fmlasucdisj  35891  satffunlem  35893  satffunlem2lem1  35896  ex-sategoelel12  35919  rankeq1o  36663  bj-pr2val  37654  bj-2upln1upl  37660  rhmpsr1  43316  pw2f1ocnv  43764  oenord1ex  44042  oenord1  44043  cantnfresb  44051  clsk3nimkb  44766  clsk1indlem4  44770  f1omo  49671  f1omoOLD  49672  f1omoALT  49673  nelsubc3  49849  indthinc  50240  indthincALT  50241  prsthinc  50242  setc1obas  50270  setc1ohomfval  50271  setc1oid  50273  isinito2lem  50276  isinito3  50278  prstchom  50340  prstchom2ALT  50342  setc1onsubc  50380  cnelsubc  50382