Theorem 1oex 8495

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

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

Step	Hyp	Ref	Expression
1		df1o2 8492	. 2 ⊢ 1o = {∅}
2		snex 5411	. 2 ⊢ {∅} ∈ V
3	1, 2	eqeltri 2831	1 ⊢ 1o ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3464  ∅c0 4313  {csn 4606  1_oc1o 8478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-dif 3934  df-un 3936  df-nul 4314  df-sn 4607  df-pr 4609  df-suc 6363  df-1o 8485

This theorem is referenced by:  1on  8497  nlim2  8507  oev  8531  oe0  8539  oev2  8540  oneo  8598  nnneo  8672  enpr2d  9068  endisj  9077  map2xp  9166  snnen2o  9250  sdom1  9255  sdom1OLD  9256  rex2dom  9259  1sdom2dom  9260  1sdomOLD  9262  ssttrcl  9734  ttrclselem2  9745  djuexb  9928  djurcl  9930  djurf1o  9932  djuss  9939  djuun  9945  1stinr  9948  2ndinr  9949  pm54.43  10020  dju1dif  10192  djucomen  10197  djuassen  10198  infdju1  10209  pwdju1  10210  nnadju  10217  infmap2  10236  cfsuc  10276  isfin4p1  10334  dcomex  10466  pwcfsdom  10602  cfpwsdom  10603  canthp1lem2  10672  pwxpndom2  10684  indpi  10926  pinq  10946  archnq  10999  sadcf  16477  sadcp1  16479  fnpr2ob  17577  xpsfrnel  17581  xpsle  17598  setcepi  18106  setc2obas  18112  setc2ohom  18113  efgi1  19707  frgpuptinv  19757  dmdprdpr  20037  dprdpr  20038  coe1fval3  22149  00ply1bas  22180  ply1plusgfvi  22182  coe1z  22205  coe1tm  22215  ply1vscl  22327  rhmply1  22329  rhmply1vr1  22330  xpstopnlem1  23752  xpstopnlem2  23754  xpsdsval  24325  nofv  27626  noxp1o  27632  noextendlt  27638  bdayfo  27646  nosep1o  27650  nosepdmlem  27652  nolt02o  27664  nogt01o  27665  nosupbnd1lem5  27681  nosupbnd2lem1  27684  noinfno  27687  noinfbday  27689  noinfbnd1  27698  noinfbnd2lem1  27699  noinfbnd2  27700  noetasuplem1  27702  noetasuplem2  27703  noetasuplem4  27705  fply1  33576  gonanegoal  35379  fmlaomn0  35417  gonan0  35419  gonarlem  35421  gonar  35422  fmlasucdisj  35426  satffunlem  35428  satffunlem2lem1  35431  ex-sategoelel12  35454  rankeq1o  36194  bj-pr2val  37041  bj-2upln1upl  37047  rhmpsr1  42551  pw2f1ocnv  43036  omnord1ex  43303  oege2  43306  oenord1ex  43314  oenord1  43315  oaomoencom  43316  oenassex  43317  cantnfresb  43323  omcl3g  43333  clsk3nimkb  44039  clsk1indlem4  44043  clsk1indlem1  44044  f1omo  48848  f1omoALT  48849  nelsubc3  49018  indthinc  49328  indthincALT  49329  prsthinc  49330  setc1obas  49357  setc1ohomfval  49358  setc1oid  49360  isinito2lem  49363  isinito3  49365  prstchom  49419  prstchom2ALT  49421  setc1onsubc  49459  cnelsubc  49461