Theorem sumeq1d 15666

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-xp 5644  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-iota 6464  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-oprab 7391  df-mpo 7392  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-seq 13967  df-sum 15653

This theorem is referenced by:  sumeq12dv  15672  sumeq12rdv  15673  fsumf1o  15689  sumss  15690  fsumcllem  15698  fsumsplit1  15711  fsum1  15713  fzosump1  15718  fsump1  15722  fsum2d  15737  fsumcom2  15740  fsumshftm  15747  fsumrev2  15748  telfsumo  15768  telfsum  15770  telfsum2  15771  fsumparts  15772  fsumiun  15787  bcxmas  15801  incexclem  15802  incexc2  15804  isumsplit  15806  isum1p  15807  arisum  15826  arisum2  15827  geoser  15833  pwdif  15834  geolim  15836  geo2sum2  15840  mertenslem1  15850  mertenslem2  15851  mertens  15852  bpolydiflem  16020  efcvgfsum  16052  fprodefsum  16061  eftlub  16077  effsumlt  16079  eirrlem  16172  pwp1fsum  16361  bitsinv1  16412  bitsinvp1  16419  pcfac  16870  prmreclem4  16890  prmreclem6  16892  ovoliunlem1  25403  uniioombllem3  25486  itg11  25592  dvfsumlem1  25932  dvfsumlem4  25936  dvfsum2  25941  elplyr  26106  coeeu  26130  coeeq  26132  plyco  26146  0dgrb  26151  dvply2g  26192  dvply2gOLD  26193  vieta1lem2  26219  vieta1  26220  aaliou3lem5  26255  aaliou3lem6  26256  aaliou3lem7  26257  taylpfval  26272  pserdvlem2  26338  abelthlem6  26346  logfac  26510  advlogexp  26564  emcllem2  26907  emcllem3  26908  emcllem7  26912  harmonicbnd  26914  harmonicbnd2  26915  harmonicbnd3  26918  harmonicbnd4  26921  chtval  27020  chpval  27032  chtfl  27059  chpfl  27060  chtprm  27063  chtnprm  27064  chpp1  27065  chtdif  27068  prmorcht  27088  musum  27101  muinv  27103  logfaclbnd  27133  logfacbnd3  27134  logexprlim  27136  chtppilimlem1  27384  rplogsumlem2  27396  rpvmasumlem  27398  dchrisumlem1  27400  dchrisumlem2  27401  dchrisumlem3  27402  dchrisum  27403  dchrisum0fval  27416  dchrisum0ff  27418  dchrisum0flblem1  27419  dchrisum0lem2  27429  dchrisum0  27431  mulog2sumlem1  27445  2vmadivsumlem  27451  log2sumbnd  27455  logdivbnd  27467  selberg3lem1  27468  pntrsumbnd  27477  pntrsumbnd2  27478  pntrlog2bndlem1  27488  pntrlog2bndlem4  27491  pntpbnd1  27497  pntpbnd2  27498  pntlemf  27516  brcgr  28827  axlowdimlem16  28884  eengv  28906  finsumvtxdg2sstep  29477  eulerpartlemgs2  34371  signsvfn  34573  fsum2dsub  34598  reprval  34601  reprsuc  34606  hashrepr  34616  chpvalz  34619  chtvalz  34620  breprexplema  34621  breprexplemc  34623  breprexp  34624  breprexpnat  34625  vtsval  34628  circlemeth  34631  hgt750lemb  34647  hgt750lema  34648  tgoldbachgtda  34652  tgoldbachgt  34654  subfacval2  35174  subfaclim  35175  bccolsum  35726  sumeq12sdv  36205  knoppndvlem6  36505  mettrifi  37751  rrncmslem  37826  sticksstones6  42139  sticksstones7  42140  sticksstones8  42141  sticksstones9  42142  sticksstones10  42143  sticksstones11  42144  sticksstones12a  42145  sticksstones12  42146  sticksstones16  42150  unitscyglem2  42184  unitscyglem4  42186  fzosumm1  42238  fz1sump1  42298  sumcubes  42301  k0004val  44139  binomcxplemnn0  44338  fsumnncl  45570  fsumiunss  45573  fsumsermpt  45577  sumnnodd  45628  dvnmul  45941  dvnprodlem3  45946  itgspltprt  45977  stoweidlem17  46015  stoweidlem20  46018  stirlinglem12  46083  dirkertrigeqlem1  46096  dirkertrigeqlem3  46098  fourierdlem83  46187  fourierdlem112  46216  fourierdlem113  46217  elaa2lem  46231  etransclem32  46264  sge00  46374  sge0iunmptlemre  46413  sge0reuzb  46446  meaiuninclem  46478  carageniuncllem1  46519  hoidmvlelem3  46595  nnsum3primes4  47789  nnsum3primesprm  47791  nnsum3primesgbe  47793  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  wtgoldbnnsum4prm  47803  bgoldbnnsum3prm  47805  altgsumbcALT  48341  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  nn0sumshdiglem1  48610  nn0sumshdiglem2  48611