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

Theorem c0ex 10623
Description: Zero is a set. (Contributed by David A. Wheeler, 7-Jul-2016.)
Assertion
Ref Expression
c0ex 0 ∈ V

Proof of Theorem c0ex
StepHypRef Expression
1 0cn 10621 . 2 0 ∈ ℂ
21elexi 3511 1 0 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  Vcvv 3492  cc 10523  0cc0 10525
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-mulcl 10587  ax-i2m1 10593
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-v 3494
This theorem is referenced by:  ofsubeq0  11623  ofsubge0  11625  elnn0  11887  un0mulcl  11919  frnnn0supp  11941  frnnn0fsupp  11942  nn0ssz  11991  nn0ind-raph  12070  xaddval  12604  xmulval  12606  ser0f  13411  facnn  13623  fac0  13624  bcval  13652  prhash2ex  13748  wrdexb  13861  s1rn  13941  eqs1  13954  repsw1  14133  cshw1  14172  s1co  14183  funcnvs2  14263  funcnvs3  14264  funcnvs4  14265  wrdlen2i  14292  wrd2pr2op  14293  wrd3tpop  14298  wwlktovf1  14309  wrdl3s3  14314  sgnval  14435  iserge0  15005  sum0  15066  sumz  15067  fsumss  15070  fsumser  15075  isumless  15188  geomulcvg  15220  rpnnen2lem1  15555  ruclem4  15575  ruclem8  15578  ruclem11  15581  0bits  15776  gcdval  15833  lcmval  15924  lcmfpr  15959  lcmfunsnlem2  15972  prmreclem2  16241  prmreclem5  16244  vdwapun  16298  mgmnsgrpex  18034  odval  18591  odf  18594  gexval  18632  telgsumfz0  19041  telgsum  19043  srgbinom  19224  abvtrivd  19540  snifpsrbag  20074  psrbaglesupp  20076  psrbagaddcl  20078  psrbaglefi  20080  mplcoe5  20177  mplbas2  20179  ltbwe  20181  psrbag0  20202  psrbagev1  20218  cply1coe0bi  20396  m2cpminvid2lem  21290  pmatcollpw3fi1lem1  21322  pmatcollpw3fi1lem2  21323  pmatcollpw3fi1  21324  idpm2idmp  21337  prdsdsf  22904  prdsxmetlem  22905  prdsmet  22907  imasdsf1olem  22910  prdsbl  23028  xrge0gsumle  23368  xrge0tsms  23369  xrhmeo  23477  pcopt  23553  pcopt2  23554  pcoass  23555  rrxcph  23922  rrx0el  23928  rrxbasefi  23940  ovoliunnul  24035  ovolicc1  24044  vitalilem5  24140  mbfpos  24179  0pval  24199  0pledm  24201  i1f1lem  24217  i1f1  24218  itg11  24219  itg1addlem3  24226  itg1addlem4  24227  i1fres  24233  itg1climres  24242  mbfi1fseqlem4  24246  mbfi1fseqlem6  24248  mbfi1flimlem  24250  mbfi1flim  24251  xrge0f  24259  itg2ge0  24263  itg2uba  24271  itg2splitlem  24276  itg2monolem1  24278  itg2gt0  24288  itg2cnlem1  24289  ibl0  24314  iblcnlem1  24315  i1fibl  24335  itgeqa  24341  itgcn  24370  dvcmul  24468  dvcmulf  24469  dvexp3  24502  dvef  24504  rolle  24514  dveq0  24524  dv11cn  24525  tdeglem4  24581  elply2  24713  elplyd  24719  ply1term  24721  ply0  24725  plyeq0  24728  plypf1  24729  plymullem  24733  dgrlt  24783  plymul0or  24797  dvply1  24800  plydivlem4  24812  elqaalem2  24836  iaa  24841  aareccl  24842  aannenlem2  24845  tayl0  24877  taylpfval  24880  dvtaylp  24885  pserdvlem2  24943  abelthlem9  24955  logtayl  25170  cxplogb  25291  leibpilem2  25446  leibpi  25447  jensenlem2  25492  jensen  25493  amgmlem  25494  amgm  25495  igamval  25551  vmaval  25617  vmaf  25623  muval  25636  dchrelbas2  25740  dchrinvcl  25756  dchrptlem2  25768  lgseisenlem4  25881  addsqnreup  25946  pntrlog2bndlem4  26083  pntrlog2bndlem5  26084  padicval  26120  padicabv  26133  ostth1  26136  axlowdimlem8  26662  axlowdimlem9  26663  axlowdimlem10  26664  axlowdimlem11  26665  axlowdimlem12  26666  axlowdimlem13  26667  axlowdimlem17  26671  uspgr1ewop  26957  usgr2v1e2w  26961  umgr2v2eedg  27233  umgr2v2e  27234  umgr2v2evd2  27236  wlkl1loop  27346  2wlklem  27376  usgr2trlncl  27468  2wlkdlem4  27634  2wlkdlem5  27635  2pthdlem1  27636  2wlkdlem10  27641  umgrwwlks2on  27663  rusgrnumwwlkl1  27674  clwwlkn2  27749  0spth  27832  1wlkdlem4  27846  wlk2v2elem1  27861  3wlkdlem4  27868  3wlkdlem5  27869  3pthdlem1  27870  3wlkdlem10  27875  upgr3v3e3cycl  27886  upgr4cycl4dv4e  27891  eulerpathpr  27946  konigsberglem4  27961  konigsberglem5  27962  wlkl0  28073  occllem  29007  0cnfn  29684  0lnfn  29689  nmfn0  29691  nmcexi  29730  nlelchi  29765  fprodex01  30468  s2rn  30547  s3rn  30549  xrge0tsmsd  30619  cyc2fv1  30690  cyc3fv1  30706  cyc3evpm  30719  sgnsval  30730  sgnsf  30731  xrge0iif1  31080  xrge0mulc1cn  31083  gsumesum  31217  esumpfinval  31233  esumpfinvalf  31234  ddeval1  31392  ddeval0  31393  ddemeas  31394  eulerpartlemt  31528  coinfliprv  31639  sgncl  31695  plymul02  31715  plymulx  31717  signsw0glem  31722  signsw0g  31725  signswmnd  31726  signswrid  31727  prodfzo03  31773  circlevma  31812  circlemethhgt  31813  hgt750lemg  31824  hgt750lemb  31826  hgt750lema  31827  hgt750leme  31828  tgoldbachgtde  31830  tgoldbachgt  31833  cvmliftlem4  32432  cvmliftlem5  32433  poimirlem1  34774  poimirlem2  34775  poimirlem3  34776  poimirlem4  34777  poimirlem5  34778  poimirlem6  34779  poimirlem7  34780  poimirlem11  34784  poimirlem12  34785  poimirlem16  34789  poimirlem17  34790  poimirlem19  34792  poimirlem20  34793  poimirlem22  34795  poimirlem23  34796  poimirlem24  34797  poimirlem25  34798  poimirlem28  34801  poimirlem29  34802  poimirlem31  34804  poimirlem32  34805  poimir  34806  broucube  34807  mblfinlem2  34811  mblfinlem3  34812  ismblfin  34814  itg2addnclem  34824  itg2addnclem3  34826  itg2addnc  34827  ftc1anclem3  34850  ftc1anclem5  34852  ftc1anclem7  34854  ftc1anclem8  34855  ftc1anc  34856  dvacos  34860  prdsbnd  34952  heiborlem10  34979  renegclALT  35979  0prjspnlem  39146  0prjspnrel  39147  diophrw  39234  monotoddzzfi  39417  zindbi  39421  mncn0  39617  aaitgo  39640  flcidc  39652  dfrcl4  39899  fvrcllb0d  39916  fvrcllb0da  39917  iunrelexp0  39925  corclrcl  39930  relexp0idm  39938  dfrtrcl4  39961  corcltrcl  39962  cotrclrcl  39965  ofsubid  40533  lhe4.4ex1a  40538  dvsconst  40539  dvconstbi  40543  binomcxplemnn0  40558  binomcxplemdvbinom  40562  binomcxplemnotnn0  40565  n0p  41182  climrec  41760  limsup10exlem  41929  dvnmptdivc  42099  dvnmul  42104  stoweidlem55  42217  fourierdlem62  42330  fourierdlem104  42372  fouriersw  42393  ovnval2  42704  hoidmvval  42736  fun2dmnopgexmpl  43360  el1fzopredsuc  43402  nn0mnd  43963  smndex1n0mnd  44012  zlmodzxzel  44331  zlmodzxz0  44332  zlmodzxzscm  44333  zlmodzxzadd  44334  zlmodzxznm  44480  zlmodzxzldeplem  44481  zlmodzxzldeplem2  44484  blen0  44560  nn0sumshdiglemB  44608  ehl2eudisval0  44640  2sphere0  44665  line2ylem  44666  line2  44667  line2x  44669  line2y  44670  ex-gt  44755  ex-gte  44756  aacllem  44830
  Copyright terms: Public domain W3C validator