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

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

Proof of Theorem c0ex
StepHypRef Expression
1 0cn 9040 . 2  |-  0  e.  CC
21elexi 2925 1  |-  0  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1721   _Vcvv 2916   CCcc 8944   0cc0 8946
This theorem is referenced by:  ofsubeq0  9953  ofsubge0  9955  elnn0  10179  un0mulcl  10210  nn0ssz  10258  nn0ind-raph  10326  xaddval  10765  xmulval  10767  ser0f  11331  facnn  11523  fac0  11524  bcval  11550  wrdexb  11718  s1co  11757  iserge0  12409  sum0  12470  sumz  12471  fsumss  12474  fsumser  12479  isumless  12580  geomulcvg  12608  rpnnen2lem1  12769  ruclem4  12788  ruclem8  12791  0bits  12906  gcdval  12963  prmreclem2  13240  prmreclem5  13243  vdwapun  13297  odval  15127  odf  15130  gexval  15167  abvtrivd  15883  psrbag0  16509  prdsdsf  18350  prdsxmetlem  18351  prdsmet  18353  prdsbl  18474  xrhmeo  18924  pcopt  19000  pcopt2  19001  pcoass  19002  ovoliunnul  19356  ovolicc1  19365  vitalilem5  19457  mbfpos  19496  0pval  19516  0pledm  19518  i1f1lem  19534  i1f1  19535  itg11  19536  itg1addlem3  19543  itg1addlem4  19544  i1fres  19550  itg1climres  19559  mbfi1fseqlem4  19563  mbfi1fseqlem6  19565  mbfi1flimlem  19567  mbfi1flim  19568  xrge0f  19576  itg2ge0  19580  itg2uba  19588  itg2splitlem  19593  itg2monolem1  19595  itg2gt0  19605  itg2cnlem1  19606  ibl0  19631  i1fibl  19652  itgeqa  19658  itgcn  19687  dvcmul  19783  dvcmulf  19784  dvexp3  19815  rolle  19827  dveq0  19837  dv11cn  19838  tdeglem4  19936  elply2  20068  elplyd  20074  ply1term  20076  ply0  20080  plyeq0  20083  plymullem  20088  dgrlt  20137  plymul0or  20151  dvply1  20154  plydivlem4  20166  elqaalem2  20190  aareccl  20196  aannenlem2  20199  dvtaylp  20239  pserdvlem2  20297  abelthlem9  20309  logtayl  20504  leibpilem2  20734  leibpi  20735  vmaval  20849  vmaf  20855  muval  20868  dchrelbas2  20974  dchrinvcl  20990  dchrptlem2  21002  pntrlog2bndlem4  21227  pntrlog2bndlem5  21228  padicval  21264  padicabv  21277  ostth1  21280  2trllemA  21503  2trllemH  21505  2trllemE  21506  2wlklemA  21507  wlkntrllem1  21512  wlkntrllem2  21513  wlkntrllem3  21514  2wlklem  21517  0spth  21524  constr1trl  21541  1pthon  21544  2pthlem2  21549  2wlklem1  21550  2pthon  21555  2pthon3v  21557  constr3lem2  21586  constr3lem4  21587  constr3lem5  21588  constr3trllem1  21590  constr3trllem2  21591  eupath  21656  occllem  22758  0cnfn  23436  0lnfn  23441  nmfn0  23443  nmcexi  23482  nlelchi  23517  xrge0iif1  24277  xrge0mulc1cn  24280  coinfliprv  24693  igamval  24784  cvmliftlem4  24928  cvmliftlem5  24929  relexp0  25082  axlowdimlem8  25792  axlowdimlem9  25793  axlowdimlem10  25794  axlowdimlem11  25795  axlowdimlem12  25796  axlowdimlem13  25797  axlowdimlem17  25801  mblfinlem  26143  mblfinlem2  26144  ismblfin  26146  itg2addnclem  26155  itg2addnclem3  26157  itg2addnc  26158  prdsbnd  26392  heiborlem10  26419  diophrw  26707  monotoddzzfi  26895  zindbi  26899  mncn0  27212  aaitgo  27235  flcidc  27247  ofsubid  27409  lhe4.4ex1a  27414  dvsconst  27415  dvconstbi  27419  climrec  27596  stoweidlem55  27671  usgra2pthspth  28035  usgra2wlkspthlem1  28036  usgra2wlkspthlem2  28037  usgra2pthlem1  28040  usgra2pth  28041  usgra2adedglem1  28048  usg2wlkonot  28080  usg2wotspth  28081  ex-gt  28185  ex-gte  28186  sgnval  28232
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-mulcl 9008  ax-i2m1 9014
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-v 2918
  Copyright terms: Public domain W3C validator