MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  c0ex Structured version   Unicode version

Theorem c0ex 9607
Description: 0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
Assertion
Ref Expression
c0ex  |-  0  e.  _V

Proof of Theorem c0ex
StepHypRef Expression
1 0cn 9605 . 2  |-  0  e.  CC
21elexi 3119 1  |-  0  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1819   _Vcvv 3109   CCcc 9507   0cc0 9509
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-12 1855  ax-ext 2435  ax-1cn 9567  ax-icn 9568  ax-addcl 9569  ax-mulcl 9571  ax-i2m1 9577
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111
This theorem is referenced by:  ofsubeq0  10553  ofsubge0  10555  elnn0  10818  un0mulcl  10851  frnnn0supp  10870  frnnn0fsupp  10872  nn0ssz  10906  nn0ind-raph  10985  xaddval  11447  xmulval  11449  ser0f  12162  facnn  12357  fac0  12358  bcval  12384  prhash2ex  12467  snopiswrd  12562  wrdexb  12564  s1rn  12619  eqs1  12629  repsw1  12766  cshw1  12801  s1co  12810  wrdlen2i  12895  wrd2pr2op  12896  wwlktovf1  12906  sgnval  12932  iserge0  13494  sum0  13554  sumz  13555  fsumss  13558  fsumser  13563  isumless  13668  geomulcvg  13696  rpnnen2lem1  13959  ruclem4  13978  ruclem8  13981  ruclem11  13984  0bits  14100  gcdval  14157  prmreclem2  14446  prmreclem5  14449  vdwapun  14503  mgmnsgrpex  16175  odval  16684  odf  16687  gexval  16724  telgsumfz0  17147  telgsum  17149  srgbinom  17322  abvtrivd  17615  snifpsrbag  18141  psrbaglesupp  18143  psrbagaddcl  18146  psrbaglefi  18149  mplcoe5  18257  mplbas2  18260  ltbwe  18263  psrbag0  18285  psrbagev1  18303  cply1coe0bi  18468  m2cpminvid2lem  19381  pmatcollpw3fi1lem1  19413  pmatcollpw3fi1lem2  19414  pmatcollpw3fi1  19415  idpm2idmp  19428  prdsdsf  20995  prdsxmetlem  20996  prdsmet  20998  imasdsf1olem  21001  prdsbl  21119  xrge0gsumle  21463  xrge0tsms  21464  xrhmeo  21571  pcopt  21647  pcopt2  21648  pcoass  21649  rrxcph  21949  ovoliunnul  22043  ovolicc1  22052  vitalilem5  22146  mbfpos  22183  0pval  22203  0pledm  22205  i1f1lem  22221  i1f1  22222  itg11  22223  itg1addlem3  22230  itg1addlem4  22231  i1fres  22237  itg1climres  22246  mbfi1fseqlem4  22250  mbfi1fseqlem6  22252  mbfi1flimlem  22254  mbfi1flim  22255  xrge0f  22263  itg2ge0  22267  itg2uba  22275  itg2splitlem  22280  itg2monolem1  22282  itg2gt0  22292  itg2cnlem1  22293  ibl0  22318  iblcnlem1  22319  i1fibl  22339  itgeqa  22345  itgcn  22374  dvcmul  22472  dvcmulf  22473  dvexp3  22504  rolle  22516  dveq0  22526  dv11cn  22527  tdeglem4  22583  elply2  22718  elplyd  22724  ply1term  22726  ply0  22730  plyeq0  22733  plypf1  22734  plymullem  22738  dgrlt  22788  plymul0or  22802  dvply1  22805  plydivlem4  22817  elqaalem2  22841  iaa  22846  aareccl  22847  aannenlem2  22850  tayl0  22882  taylpfval  22885  dvtaylp  22890  pserdvlem2  22948  abelthlem9  22960  logtayl  23166  leibpilem2  23397  leibpi  23398  jensenlem2  23442  jensen  23443  amgmlem  23444  amgm  23445  vmaval  23512  vmaf  23518  muval  23531  dchrelbas2  23637  dchrinvcl  23653  dchrptlem2  23665  lgseisenlem4  23752  pntrlog2bndlem4  23890  pntrlog2bndlem5  23891  padicval  23927  padicabv  23940  ostth1  23943  axlowdimlem8  24378  axlowdimlem9  24379  axlowdimlem10  24380  axlowdimlem11  24381  axlowdimlem12  24382  axlowdimlem13  24383  axlowdimlem17  24387  2trllemA  24678  2trllemH  24680  2trllemE  24681  2wlklemA  24682  wlkntrllem1  24687  wlkntrllem2  24688  wlkntrllem3  24689  2wlklem  24692  0spth  24699  constr1trl  24716  1pthon  24719  2pthlem2  24724  2wlklem1  24725  2pthon  24730  2pthon3v  24732  usgra2adedgwlkonALT  24742  usgra2wlkspthlem1  24745  usgra2wlkspthlem2  24746  constr3lem2  24772  constr3lem4  24773  constr3lem5  24774  constr3trllem1  24776  constr3trllem2  24777  clwwlkn2  24901  usg2wlkonot  25009  usg2wotspth  25010  0egra0rgra  25062  rusgranumwlkl1  25073  eupath  25107  occllem  26347  0cnfn  27025  0lnfn  27030  nmfn0  27032  nmcexi  27071  nlelchi  27106  xrge0infss  27730  sgnsval  27870  sgnsf  27871  xrge0tsmsd  27928  xrge0iif1  28073  xrge0mulc1cn  28076  gsumesum  28222  esumpfinval  28237  esumpfinvalf  28238  ddeval1  28367  ddeval0  28368  ddemeas  28369  eulerpartlemt  28485  coinfliprv  28596  sgncl  28652  plymul02  28678  plymulx  28680  signsw0glem  28685  signsw0g  28688  signswmnd  28689  signswrid  28690  signstfvn  28701  igamval  28764  cvmliftlem4  28908  cvmliftlem5  28909  relexp0  29227  mblfinlem2  30214  mblfinlem3  30215  ismblfin  30217  itg2addnclem  30228  itg2addnclem3  30230  itg2addnc  30231  ftc1anclem3  30254  ftc1anclem5  30256  ftc1anclem7  30258  ftc1anclem8  30259  ftc1anc  30260  dvacos  30266  prdsbnd  30451  heiborlem10  30478  diophrw  30854  monotoddzzfi  31040  zindbi  31044  mncn0  31250  aaitgo  31273  flcidc  31285  lcmval  31360  ofsubid  31391  lhe4.4ex1a  31396  dvsconst  31397  dvconstbi  31401  binomcxplemnn0  31416  binomcxplemdvbinom  31420  binomcxplemnotnn0  31423  n0p  31598  climrec  31770  dvnmptdivc  31896  dvnmul  31901  stoweidlem55  31998  fourierdlem62  32112  fourierdlem104  32154  fouriersw  32175  usgra2adedglem1  32576  zlmodzxzel  33046  zlmodzxz0  33047  zlmodzxzscm  33048  zlmodzxzadd  33049  zlmodzxznm  33200  zlmodzxzldeplem  33201  zlmodzxzldeplem2  33204  ex-gt  33224  ex-gte  33225  aacllem  33318  renegclALT  34795
  Copyright terms: Public domain W3C validator