Theorem 1oex 8515

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

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

Step	Hyp	Ref	Expression
1		df1o2 8512	. 2 ⊢ 1o = {∅}
2		snex 5442	. 2 ⊢ {∅} ∈ V
3	1, 2	eqeltri 2835	1 ⊢ 1o ∈ V

Syntax hints:   ∈ wcel 2106  Vcvv 3478  ∅c0 4339  {csn 4631  1_oc1o 8498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-dif 3966  df-un 3968  df-nul 4340  df-sn 4632  df-pr 4634  df-suc 6392  df-1o 8505

This theorem is referenced by:  1on  8517  nlim2  8527  oev  8551  oe0  8559  oev2  8560  oneo  8618  nnneo  8692  enpr2d  9088  endisj  9097  map2xp  9186  snnen2o  9271  sdom1  9276  sdom1OLD  9277  rex2dom  9280  1sdom2dom  9281  1sdomOLD  9283  ssttrcl  9753  ttrclselem2  9764  djuexb  9947  djurcl  9949  djurf1o  9951  djuss  9958  djuun  9964  1stinr  9967  2ndinr  9968  pm54.43  10039  dju1dif  10211  djucomen  10216  djuassen  10217  infdju1  10228  pwdju1  10229  nnadju  10236  infmap2  10255  cfsuc  10295  isfin4p1  10353  dcomex  10485  pwcfsdom  10621  cfpwsdom  10622  canthp1lem2  10691  pwxpndom2  10703  indpi  10945  pinq  10965  archnq  11018  sadcf  16487  sadcp1  16489  fnpr2ob  17605  xpsfrnel  17609  xpsle  17626  setcepi  18142  setc2obas  18148  setc2ohom  18149  efgi1  19754  frgpuptinv  19804  dmdprdpr  20084  dprdpr  20085  coe1fval3  22226  00ply1bas  22257  ply1plusgfvi  22259  coe1z  22282  coe1tm  22292  ply1vscl  22404  rhmply1  22406  rhmply1vr1  22407  xpstopnlem1  23833  xpstopnlem2  23835  xpsdsval  24407  nofv  27717  noxp1o  27723  noextendlt  27729  bdayfo  27737  nosep1o  27741  nosepdmlem  27743  nolt02o  27755  nogt01o  27756  nosupbnd1lem5  27772  nosupbnd2lem1  27775  noinfno  27778  noinfbday  27780  noinfbnd1  27789  noinfbnd2lem1  27790  noinfbnd2  27791  noetasuplem1  27793  noetasuplem2  27794  noetasuplem4  27796  fply1  33564  gonanegoal  35337  fmlaomn0  35375  gonan0  35377  gonarlem  35379  gonar  35380  fmlasucdisj  35384  satffunlem  35386  satffunlem2lem1  35389  ex-sategoelel12  35412  rankeq1o  36153  bj-pr2val  37001  bj-2upln1upl  37007  rhmpsr1  42540  pw2f1ocnv  43026  omnord1ex  43294  oege2  43297  oenord1ex  43305  oenord1  43306  oaomoencom  43307  oenassex  43308  cantnfresb  43314  omcl3g  43324  clsk3nimkb  44030  clsk1indlem4  44034  clsk1indlem1  44035  f1omo  48691  f1omoALT  48692  indthinc  48853  indthincALT  48854  prsthinc  48855  prstchom  48878  prstchom2ALT  48880