Theorem sumeq1d 15644

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 15632	. 2 ⊢ (𝐴 = 𝐵 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶)
3	1, 2	syl 17	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶)

Syntax hints:   → wi 4   = wceq 1533  Σcsu 15629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-opab 5201  df-mpt 5222  df-xp 5672  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-iota 6485  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7404  df-oprab 7405  df-mpo 7406  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-seq 13964  df-sum 15630

This theorem is referenced by:  sumeq12dv  15649  sumeq12rdv  15650  fsumf1o  15666  sumss  15667  fsumcllem  15675  fsumsplit1  15688  fsum1  15690  fzosump1  15695  fsump1  15699  fsum2d  15714  fsumcom2  15717  fsumshftm  15724  fsumrev2  15725  telfsumo  15745  telfsum  15747  telfsum2  15748  fsumparts  15749  fsumiun  15764  bcxmas  15778  incexclem  15779  incexc2  15781  isumsplit  15783  isum1p  15784  arisum  15803  arisum2  15804  geoser  15810  pwdif  15811  geolim  15813  geo2sum2  15817  mertenslem1  15827  mertenslem2  15828  mertens  15829  bpolydiflem  15995  efcvgfsum  16026  fprodefsum  16035  eftlub  16049  effsumlt  16051  eirrlem  16144  pwp1fsum  16331  bitsinv1  16380  bitsinvp1  16387  pcfac  16831  prmreclem4  16851  prmreclem6  16853  ovoliunlem1  25353  uniioombllem3  25436  itg11  25542  dvfsumlem1  25882  dvfsumlem4  25886  dvfsum2  25891  elplyr  26055  coeeu  26079  coeeq  26081  plyco  26095  0dgrb  26100  dvply2g  26139  vieta1lem2  26165  vieta1  26166  aaliou3lem5  26201  aaliou3lem6  26202  aaliou3lem7  26203  taylpfval  26218  pserdvlem2  26282  abelthlem6  26290  logfac  26451  advlogexp  26505  emcllem2  26845  emcllem3  26846  emcllem7  26850  harmonicbnd  26852  harmonicbnd2  26853  harmonicbnd3  26856  harmonicbnd4  26859  chtval  26958  chpval  26970  chtfl  26997  chpfl  26998  chtprm  27001  chtnprm  27002  chpp1  27003  chtdif  27006  prmorcht  27026  musum  27039  muinv  27041  logfaclbnd  27071  logfacbnd3  27072  logexprlim  27074  chtppilimlem1  27322  rplogsumlem2  27334  rpvmasumlem  27336  dchrisumlem1  27338  dchrisumlem2  27339  dchrisumlem3  27340  dchrisum  27341  dchrisum0fval  27354  dchrisum0ff  27356  dchrisum0flblem1  27357  dchrisum0lem2  27367  dchrisum0  27369  mulog2sumlem1  27383  2vmadivsumlem  27389  log2sumbnd  27393  logdivbnd  27405  selberg3lem1  27406  pntrsumbnd  27415  pntrsumbnd2  27416  pntrlog2bndlem1  27426  pntrlog2bndlem4  27429  pntpbnd1  27435  pntpbnd2  27436  pntlemf  27454  brcgr  28627  axlowdimlem16  28684  eengv  28706  finsumvtxdg2sstep  29275  eulerpartlemgs2  33868  signsvfn  34082  fsum2dsub  34108  reprval  34111  reprsuc  34116  hashrepr  34126  chpvalz  34129  chtvalz  34130  breprexplema  34131  breprexplemc  34133  breprexp  34134  breprexpnat  34135  vtsval  34138  circlemeth  34141  hgt750lemb  34157  hgt750lema  34158  tgoldbachgtda  34162  tgoldbachgt  34164  subfacval2  34667  subfaclim  34668  bccolsum  35204  knoppndvlem6  35883  mettrifi  37115  rrncmslem  37190  sticksstones6  41460  sticksstones7  41461  sticksstones8  41462  sticksstones9  41463  sticksstones10  41464  sticksstones11  41465  sticksstones12a  41466  sticksstones12  41467  sticksstones16  41471  fzosumm1  41561  fz1sump1  41697  sumcubes  41700  k0004val  43390  binomcxplemnn0  43597  fsumnncl  44773  fsumiunss  44776  fsumsermpt  44780  sumnnodd  44831  dvnmul  45144  dvnprodlem3  45149  itgspltprt  45180  stoweidlem17  45218  stoweidlem20  45221  stirlinglem12  45286  dirkertrigeqlem1  45299  dirkertrigeqlem3  45301  fourierdlem83  45390  fourierdlem112  45419  fourierdlem113  45420  elaa2lem  45434  etransclem32  45467  sge00  45577  sge0iunmptlemre  45616  sge0reuzb  45649  meaiuninclem  45681  carageniuncllem1  45722  hoidmvlelem3  45798  nnsum3primes4  46941  nnsum3primesprm  46943  nnsum3primesgbe  46945  nnsum4primesodd  46949  nnsum4primesoddALTV  46950  wtgoldbnnsum4prm  46955  bgoldbnnsum3prm  46957  altgsumbcALT  47218  nn0sumshdiglemA  47493  nn0sumshdiglemB  47494  nn0sumshdiglem1  47495  nn0sumshdiglem2  47496