Theorem 1oex 8491

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

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

Step	Hyp	Ref	Expression
1		df1o2 8488	. 2 ⊢ 1o = {∅}
2		snex 5428	. 2 ⊢ {∅} ∈ V
3	1, 2	eqeltri 2825	1 ⊢ 1o ∈ V

Syntax hints:   ∈ wcel 2099  Vcvv 3470  ∅c0 4319  {csn 4625  1_oc1o 8474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-sep 5294  ax-nul 5301  ax-pr 5424

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3472  df-dif 3948  df-un 3950  df-nul 4320  df-sn 4626  df-pr 4628  df-suc 6370  df-1o 8481

This theorem is referenced by:  1on  8493  2oexOLD  8502  nlim2  8505  oev  8529  oe0  8537  oev2  8538  oneo  8596  nnneo  8670  enpr2d  9068  endisj  9077  map2xp  9166  snnen2o  9256  sdom1  9261  sdom1OLD  9262  rex2dom  9265  1sdom2dom  9266  1sdomOLD  9268  ssttrcl  9733  ttrclselem2  9744  djuexb  9927  djurcl  9929  djurf1o  9931  djuss  9938  djuun  9944  1stinr  9947  2ndinr  9948  pm54.43  10019  dju1dif  10190  djucomen  10195  djuassen  10196  infdju1  10207  pwdju1  10208  nnadju  10215  infmap2  10236  cfsuc  10275  isfin4p1  10333  dcomex  10465  pwcfsdom  10601  cfpwsdom  10602  canthp1lem2  10671  pwxpndom2  10683  indpi  10925  pinq  10945  archnq  10998  sadcf  16422  sadcp1  16424  fnpr2ob  17534  xpsfrnel  17538  xpsle  17555  setcepi  18071  setc2obas  18077  setc2ohom  18078  efgi1  19670  frgpuptinv  19720  dmdprdpr  20000  dprdpr  20001  coe1fval3  22121  00ply1bas  22152  ply1plusgfvi  22154  coe1z  22176  coe1tm  22186  xpstopnlem1  23707  xpstopnlem2  23709  xpsdsval  24281  nofv  27584  noxp1o  27590  noextendlt  27596  bdayfo  27604  nosep1o  27608  nosepdmlem  27610  nolt02o  27622  nogt01o  27623  nosupbnd1lem5  27639  nosupbnd2lem1  27642  noinfno  27645  noinfbday  27647  noinfbnd1  27656  noinfbnd2lem1  27657  noinfbnd2  27658  noetasuplem1  27660  noetasuplem2  27661  noetasuplem4  27663  fply1  33228  gonanegoal  34957  fmlaomn0  34995  gonan0  34997  gonarlem  34999  gonar  35000  fmlasucdisj  35004  satffunlem  35006  satffunlem2lem1  35009  ex-sategoelel12  35032  rankeq1o  35762  bj-pr2val  36492  bj-2upln1upl  36498  pw2f1ocnv  42449  omnord1ex  42724  oege2  42727  oenord1ex  42735  oenord1  42736  oaomoencom  42737  oenassex  42738  cantnfresb  42744  omcl3g  42754  clsk3nimkb  43461  clsk1indlem4  43465  clsk1indlem1  43466  f1omo  47904  f1omoALT  47905  indthinc  48049  indthincALT  48050  prsthinc  48051  prstchom  48074  prstchom2ALT  48076

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »