Theorem sumeq1d 15736

Description: Equality deduction for sum. (Contributed by NM, 1-Nov-2005.)

Hypothesis

Ref	Expression
sumeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
sumeq1d	⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶)

Proof of Theorem sumeq1d

Step	Hyp	Ref	Expression
1		sumeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		sumeq1 15725	. 2 ⊢ (𝐴 = 𝐵 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶)
3	1, 2	syl 17	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶)

Syntax hints:   → wi 4   = wceq 1540  Σcsu 15722

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-xp 5691  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-iota 6514  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-seq 14043  df-sum 15723

This theorem is referenced by:  sumeq12dv  15742  sumeq12rdv  15743  fsumf1o  15759  sumss  15760  fsumcllem  15768  fsumsplit1  15781  fsum1  15783  fzosump1  15788  fsump1  15792  fsum2d  15807  fsumcom2  15810  fsumshftm  15817  fsumrev2  15818  telfsumo  15838  telfsum  15840  telfsum2  15841  fsumparts  15842  fsumiun  15857  bcxmas  15871  incexclem  15872  incexc2  15874  isumsplit  15876  isum1p  15877  arisum  15896  arisum2  15897  geoser  15903  pwdif  15904  geolim  15906  geo2sum2  15910  mertenslem1  15920  mertenslem2  15921  mertens  15922  bpolydiflem  16090  efcvgfsum  16122  fprodefsum  16131  eftlub  16145  effsumlt  16147  eirrlem  16240  pwp1fsum  16428  bitsinv1  16479  bitsinvp1  16486  pcfac  16937  prmreclem4  16957  prmreclem6  16959  ovoliunlem1  25537  uniioombllem3  25620  itg11  25726  dvfsumlem1  26066  dvfsumlem4  26070  dvfsum2  26075  elplyr  26240  coeeu  26264  coeeq  26266  plyco  26280  0dgrb  26285  dvply2g  26326  dvply2gOLD  26327  vieta1lem2  26353  vieta1  26354  aaliou3lem5  26389  aaliou3lem6  26390  aaliou3lem7  26391  taylpfval  26406  pserdvlem2  26472  abelthlem6  26480  logfac  26643  advlogexp  26697  emcllem2  27040  emcllem3  27041  emcllem7  27045  harmonicbnd  27047  harmonicbnd2  27048  harmonicbnd3  27051  harmonicbnd4  27054  chtval  27153  chpval  27165  chtfl  27192  chpfl  27193  chtprm  27196  chtnprm  27197  chpp1  27198  chtdif  27201  prmorcht  27221  musum  27234  muinv  27236  logfaclbnd  27266  logfacbnd3  27267  logexprlim  27269  chtppilimlem1  27517  rplogsumlem2  27529  rpvmasumlem  27531  dchrisumlem1  27533  dchrisumlem2  27534  dchrisumlem3  27535  dchrisum  27536  dchrisum0fval  27549  dchrisum0ff  27551  dchrisum0flblem1  27552  dchrisum0lem2  27562  dchrisum0  27564  mulog2sumlem1  27578  2vmadivsumlem  27584  log2sumbnd  27588  logdivbnd  27600  selberg3lem1  27601  pntrsumbnd  27610  pntrsumbnd2  27611  pntrlog2bndlem1  27621  pntrlog2bndlem4  27624  pntpbnd1  27630  pntpbnd2  27631  pntlemf  27649  brcgr  28915  axlowdimlem16  28972  eengv  28994  finsumvtxdg2sstep  29567  eulerpartlemgs2  34382  signsvfn  34597  fsum2dsub  34622  reprval  34625  reprsuc  34630  hashrepr  34640  chpvalz  34643  chtvalz  34644  breprexplema  34645  breprexplemc  34647  breprexp  34648  breprexpnat  34649  vtsval  34652  circlemeth  34655  hgt750lemb  34671  hgt750lema  34672  tgoldbachgtda  34676  tgoldbachgt  34678  subfacval2  35192  subfaclim  35193  bccolsum  35739  sumeq12sdv  36218  knoppndvlem6  36518  mettrifi  37764  rrncmslem  37839  sticksstones6  42152  sticksstones7  42153  sticksstones8  42154  sticksstones9  42155  sticksstones10  42156  sticksstones11  42157  sticksstones12a  42158  sticksstones12  42159  sticksstones16  42163  unitscyglem2  42197  unitscyglem4  42199  fzosumm1  42291  fz1sump1  42344  sumcubes  42347  k0004val  44163  binomcxplemnn0  44368  fsumnncl  45587  fsumiunss  45590  fsumsermpt  45594  sumnnodd  45645  dvnmul  45958  dvnprodlem3  45963  itgspltprt  45994  stoweidlem17  46032  stoweidlem20  46035  stirlinglem12  46100  dirkertrigeqlem1  46113  dirkertrigeqlem3  46115  fourierdlem83  46204  fourierdlem112  46233  fourierdlem113  46234  elaa2lem  46248  etransclem32  46281  sge00  46391  sge0iunmptlemre  46430  sge0reuzb  46463  meaiuninclem  46495  carageniuncllem1  46536  hoidmvlelem3  46612  nnsum3primes4  47775  nnsum3primesprm  47777  nnsum3primesgbe  47779  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  wtgoldbnnsum4prm  47789  bgoldbnnsum3prm  47791  altgsumbcALT  48269  nn0sumshdiglemA  48540  nn0sumshdiglemB  48541  nn0sumshdiglem1  48542  nn0sumshdiglem2  48543