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

Theorem c0ex 9087
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 9086 . 2  |-  0  e.  CC
21elexi 2967 1  |-  0  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1726   _Vcvv 2958   CCcc 8990   0cc0 8992
This theorem is referenced by:  ofsubeq0  9999  ofsubge0  10001  elnn0  10225  un0mulcl  10256  nn0ssz  10304  nn0ind-raph  10372  xaddval  10811  xmulval  10813  ser0f  11378  facnn  11570  fac0  11571  bcval  11597  wrdexb  11765  s1co  11804  iserge0  12456  sum0  12517  sumz  12518  fsumss  12521  fsumser  12526  isumless  12627  geomulcvg  12655  rpnnen2lem1  12816  ruclem4  12835  ruclem8  12838  0bits  12953  gcdval  13010  prmreclem2  13287  prmreclem5  13290  vdwapun  13344  odval  15174  odf  15177  gexval  15214  abvtrivd  15930  psrbag0  16556  prdsdsf  18399  prdsxmetlem  18400  prdsmet  18402  prdsbl  18523  xrhmeo  18973  pcopt  19049  pcopt2  19050  pcoass  19051  ovoliunnul  19405  ovolicc1  19414  vitalilem5  19506  mbfpos  19545  0pval  19565  0pledm  19567  i1f1lem  19583  i1f1  19584  itg11  19585  itg1addlem3  19592  itg1addlem4  19593  i1fres  19599  itg1climres  19608  mbfi1fseqlem4  19612  mbfi1fseqlem6  19614  mbfi1flimlem  19616  mbfi1flim  19617  xrge0f  19625  itg2ge0  19629  itg2uba  19637  itg2splitlem  19642  itg2monolem1  19644  itg2gt0  19654  itg2cnlem1  19655  ibl0  19680  i1fibl  19701  itgeqa  19707  itgcn  19736  dvcmul  19832  dvcmulf  19833  dvexp3  19864  rolle  19876  dveq0  19886  dv11cn  19887  tdeglem4  19985  elply2  20117  elplyd  20123  ply1term  20125  ply0  20129  plyeq0  20132  plymullem  20137  dgrlt  20186  plymul0or  20200  dvply1  20203  plydivlem4  20215  elqaalem2  20239  aareccl  20245  aannenlem2  20248  dvtaylp  20288  pserdvlem2  20346  abelthlem9  20358  logtayl  20553  leibpilem2  20783  leibpi  20784  vmaval  20898  vmaf  20904  muval  20917  dchrelbas2  21023  dchrinvcl  21039  dchrptlem2  21051  pntrlog2bndlem4  21276  pntrlog2bndlem5  21277  padicval  21313  padicabv  21326  ostth1  21329  2trllemA  21552  2trllemH  21554  2trllemE  21555  2wlklemA  21556  wlkntrllem1  21561  wlkntrllem2  21562  wlkntrllem3  21563  2wlklem  21566  0spth  21573  constr1trl  21590  1pthon  21593  2pthlem2  21598  2wlklem1  21599  2pthon  21604  2pthon3v  21606  constr3lem2  21635  constr3lem4  21636  constr3lem5  21637  constr3trllem1  21639  constr3trllem2  21640  eupath  21705  occllem  22807  0cnfn  23485  0lnfn  23490  nmfn0  23492  nmcexi  23531  nlelchi  23566  xrge0iif1  24326  xrge0mulc1cn  24329  coinfliprv  24742  igamval  24833  cvmliftlem4  24977  cvmliftlem5  24978  relexp0  25131  axlowdimlem8  25890  axlowdimlem9  25891  axlowdimlem10  25892  axlowdimlem11  25893  axlowdimlem12  25894  axlowdimlem13  25895  axlowdimlem17  25899  mblfinlem2  26246  mblfinlem3  26247  ismblfin  26249  itg2addnclem  26258  itg2addnclem3  26260  itg2addnc  26261  ftc1anclem3  26284  ftc1anclem5  26286  ftc1anclem7  26288  ftc1anclem8  26289  ftc1anc  26290  prdsbnd  26504  heiborlem10  26531  diophrw  26819  monotoddzzfi  27007  zindbi  27011  mncn0  27323  aaitgo  27346  flcidc  27358  ofsubid  27520  lhe4.4ex1a  27525  dvsconst  27526  dvconstbi  27530  climrec  27707  stoweidlem55  27782  cshw1  28277  cshwssizelem1  28282  usgra2pthspth  28307  usgra2wlkspthlem1  28308  usgra2wlkspthlem2  28309  usgra2pthlem1  28312  usgra2pth  28313  usgra2adedglem1  28320  usg2wlkonot  28352  usg2wotspth  28353  0egra0rgra  28377  ex-gt  28473  ex-gte  28474  sgnval  28520
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419  ax-1cn 9050  ax-icn 9051  ax-addcl 9052  ax-mulcl 9054  ax-i2m1 9060
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-v 2960
  Copyright terms: Public domain W3C validator