Theorem sumeq1d 14279

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

Hypothesis

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

Assertion

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

Distinct variable groups:   𝐴,𝑘   𝐵,𝑘

Allowed substitution hints:   𝜑(𝑘)   𝐶(𝑘)

Proof of Theorem sumeq1d

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

Syntax hints:   → wi 4   = wceq 1475  Σcsu 14264

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-xp 5044  df-cnv 5046  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-iota 5768  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-seq 12664  df-sum 14265

This theorem is referenced by:  sumeq12dv  14284  sumeq12rdv  14285  fsumf1o  14301  sumss  14302  fsumcllem  14310  fsum1  14320  fzosump1  14325  fsump1  14329  fsum2d  14344  fsumcom2  14347  fsumcom2OLD  14348  fsumshftm  14355  fsumrev2  14356  telfsumo  14375  telfsum  14377  telfsum2  14378  fsumparts  14379  fsumiun  14394  bcxmas  14406  incexclem  14407  incexc2  14409  isumsplit  14411  isum1p  14412  arisum  14431  arisum2  14432  geoser  14438  geolim  14440  geo2sum2  14444  mertenslem1  14455  mertenslem2  14456  mertens  14457  bpolydiflem  14624  efcvgfsum  14655  fprodefsum  14664  eftlub  14678  effsumlt  14680  eirrlem  14771  pwp1fsum  14952  bitsinv1  15002  bitsinvp1  15009  pcfac  15441  prmreclem4  15461  prmreclem6  15463  ovoliunlem1  23077  uniioombllem3  23159  itg11  23264  dvfsumlem1  23593  dvfsumlem4  23596  dvfsum2  23601  elplyr  23761  coeeu  23785  coeeq  23787  plyco  23801  0dgrb  23806  dvply2g  23844  vieta1lem2  23870  vieta1  23871  aaliou3lem5  23906  aaliou3lem6  23907  aaliou3lem7  23908  taylpfval  23923  pserdvlem2  23986  abelthlem6  23994  logfac  24151  advlogexp  24201  emcllem2  24523  emcllem3  24524  emcllem7  24528  harmonicbnd  24530  harmonicbnd2  24531  harmonicbnd3  24534  harmonicbnd4  24537  chtval  24636  chpval  24648  chtfl  24675  chpfl  24676  chtprm  24679  chtnprm  24680  chpp1  24681  chtdif  24684  prmorcht  24704  musum  24717  muinv  24719  logfaclbnd  24747  logfacbnd3  24748  logexprlim  24750  chtppilimlem1  24962  rplogsumlem2  24974  rpvmasumlem  24976  dchrisumlem1  24978  dchrisumlem2  24979  dchrisumlem3  24980  dchrisum  24981  dchrisum0fval  24994  dchrisum0ff  24996  dchrisum0flblem1  24997  dchrisum0lem2  25007  dchrisum0  25009  mulog2sumlem1  25023  2vmadivsumlem  25029  log2sumbnd  25033  logdivbnd  25045  selberg3lem1  25046  pntrsumbnd  25055  pntrsumbnd2  25056  pntrlog2bndlem1  25066  pntrlog2bndlem4  25069  pntpbnd1  25075  pntpbnd2  25076  pntlemf  25094  brcgr  25580  axlowdimlem16  25637  eengv  25659  eulerpartlemgs2  29769  signsvfn  29985  subfacval2  30423  subfaclim  30424  bccolsum  30878  knoppndvlem6  31678  mettrifi  32723  rrncmslem  32801  k0004val  37468  binomcxplemnn0  37570  fsumnncl  38638  fsumsplit1  38639  fsumiunss  38642  fsumsermpt  38646  sumnnodd  38697  dvnmul  38833  dvnprodlem3  38838  itgspltprt  38871  stoweidlem17  38910  stoweidlem20  38913  stirlinglem12  38978  dirkertrigeqlem1  38991  dirkertrigeqlem3  38993  fourierdlem83  39082  fourierdlem112  39111  fourierdlem113  39112  elaa2lem  39126  etransclem32  39159  sge00  39269  sge0iunmptlemre  39308  sge0reuzb  39341  meaiuninclem  39373  carageniuncllem1  39411  hoidmvlelem3  39487  pwdif  40039  nnsum3primes4  40204  nnsum3primesprm  40206  nnsum3primesgbe  40208  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  wtgoldbnnsum4prm  40218  bgoldbnnsum3prm  40220  altgsumbcALT  41924  nn0sumshdiglemA  42211  nn0sumshdiglemB  42212  nn0sumshdiglem1  42213  nn0sumshdiglem2  42214