Theorem 1oex 8469

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

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

Step	Hyp	Ref	Expression
1		df1o2 8466	. 2 ⊢ 1o = {∅}
2		snex 5412	. 2 ⊢ {∅} ∈ V
3	1, 2	eqeltri 2861	1 ⊢ 1o ∈ V

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3457  ∅c0 4286  {csn 4591  1_oc1o 8452

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

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 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3909  df-un 3911  df-nul 4287  df-sn 4592  df-pr 4594  df-suc 6370  df-1o 8459

This theorem is used by:  1oelpr  8470  1on  8472  nlim2  8481  oev  8505  oe0  8513  oev2  8514  oneo  8572  nnneo  8647  enpr2d  9052  endisj  9059  map2xp  9142  snnen2o  9212  sdom1  9217  rex2dom  9220  1sdom2dom  9221  ssttrcl  9691  ttrclselem2  9702  djuexb  9911  djurcl  9913  djurf1o  9915  djuun  9928  1stinr  9931  2ndinr  9932  pm54.43  10003  dju1dif  10172  djucomen  10177  djuassen  10178  infdju1  10189  pwdju1  10190  nnadju  10197  infmap2  10216  cfsuc  10256  isfin4p1  10314  dcomex  10446  pwcfsdom  10583  cfpwsdom  10584  canthp1lem2  10653  pwxpndom2  10665  indpi  10907  pinq  10927  archnq  10980  sadcp1  16535  fnpr2ob  17634  xpsfrnel  17638  xpsle  17655  degenmgmopdm  19034  degenmgmnfn  19036  degenmgm  19037  degenmgm2opdm  19038  degenmgm2nfun  19039  degenmgm2  19040  dmdprdpr  20165  coe1fval3  22418  00ply1bas  22449  ply1plusgfvi  22451  coe1z  22474  coe1tm  22484  ply1vscl  22591  rhmply1  22593  rhmply1vr1  22594  xpsdsval  24589  nofv  27872  noxp1o  27878  noextendlt  27884  bdayfo  27892  nosep1o  27896  nosepdmlem  27898  nolt02o  27910  nogt01o  27911  nosupbnd1lem5  27927  nosupbnd2lem1  27930  noinfno  27933  noinfbday  27935  noinfbnd1  27944  noinfbnd2lem1  27945  noinfbnd2  27946  noetasuplem1  27948  noetasuplem2  27949  noetasuplem4  27951  fply1  33912  selvply1rhmlema  33972  selvply1rhmlemb  33973  selvply1rhmlem1  33974  selvply1rhmlem2  33975  selvply1rhmlem4  33977  selvply1rhm0  33980  gonanegoal  35881  fmlaomn0  35919  gonan0  35921  gonarlem  35923  gonar  35924  fmlasucdisj  35928  satffunlem  35930  satffunlem2lem1  35933  ex-sategoelel12  35956  rankeq1o  36700  bj-pr2val  37711  bj-2upln1upl  37717  rhmpsr1  43374  pw2f1ocnv  43822  oenord1ex  44100  oenord1  44101  cantnfresb  44109  clsk3nimkb  44824  clsk1indlem4  44828  f1omo  49728  f1omoOLD  49729  f1omoALT  49730  nelsubc3  49906  indthinc  50297  indthincALT  50298  prsthinc  50299  setc1obas  50327  setc1ohomfval  50328  setc1oid  50330  isinito2lem  50333  isinito3  50335  prstchom  50397  prstchom2ALT  50399  setc1onsubc  50437  cnelsubc  50439