Theorem sumeq1d 15716

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

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

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 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-xp 5660  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-iota 6484  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-ov 7408  df-oprab 7409  df-mpo 7410  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-seq 14020  df-sum 15703

This theorem is referenced by:  sumeq12dv  15722  sumeq12rdv  15723  fsumf1o  15739  sumss  15740  fsumcllem  15748  fsumsplit1  15761  fsum1  15763  fzosump1  15768  fsump1  15772  fsum2d  15787  fsumcom2  15790  fsumshftm  15797  fsumrev2  15798  telfsumo  15818  telfsum  15820  telfsum2  15821  fsumparts  15822  fsumiun  15837  bcxmas  15851  incexclem  15852  incexc2  15854  isumsplit  15856  isum1p  15857  arisum  15876  arisum2  15877  geoser  15883  pwdif  15884  geolim  15886  geo2sum2  15890  mertenslem1  15900  mertenslem2  15901  mertens  15902  bpolydiflem  16070  efcvgfsum  16102  fprodefsum  16111  eftlub  16127  effsumlt  16129  eirrlem  16222  pwp1fsum  16410  bitsinv1  16461  bitsinvp1  16468  pcfac  16919  prmreclem4  16939  prmreclem6  16941  ovoliunlem1  25455  uniioombllem3  25538  itg11  25644  dvfsumlem1  25984  dvfsumlem4  25988  dvfsum2  25993  elplyr  26158  coeeu  26182  coeeq  26184  plyco  26198  0dgrb  26203  dvply2g  26244  dvply2gOLD  26245  vieta1lem2  26271  vieta1  26272  aaliou3lem5  26307  aaliou3lem6  26308  aaliou3lem7  26309  taylpfval  26324  pserdvlem2  26390  abelthlem6  26398  logfac  26562  advlogexp  26616  emcllem2  26959  emcllem3  26960  emcllem7  26964  harmonicbnd  26966  harmonicbnd2  26967  harmonicbnd3  26970  harmonicbnd4  26973  chtval  27072  chpval  27084  chtfl  27111  chpfl  27112  chtprm  27115  chtnprm  27116  chpp1  27117  chtdif  27120  prmorcht  27140  musum  27153  muinv  27155  logfaclbnd  27185  logfacbnd3  27186  logexprlim  27188  chtppilimlem1  27436  rplogsumlem2  27448  rpvmasumlem  27450  dchrisumlem1  27452  dchrisumlem2  27453  dchrisumlem3  27454  dchrisum  27455  dchrisum0fval  27468  dchrisum0ff  27470  dchrisum0flblem1  27471  dchrisum0lem2  27481  dchrisum0  27483  mulog2sumlem1  27497  2vmadivsumlem  27503  log2sumbnd  27507  logdivbnd  27519  selberg3lem1  27520  pntrsumbnd  27529  pntrsumbnd2  27530  pntrlog2bndlem1  27540  pntrlog2bndlem4  27543  pntpbnd1  27549  pntpbnd2  27550  pntlemf  27568  brcgr  28879  axlowdimlem16  28936  eengv  28958  finsumvtxdg2sstep  29529  eulerpartlemgs2  34412  signsvfn  34614  fsum2dsub  34639  reprval  34642  reprsuc  34647  hashrepr  34657  chpvalz  34660  chtvalz  34661  breprexplema  34662  breprexplemc  34664  breprexp  34665  breprexpnat  34666  vtsval  34669  circlemeth  34672  hgt750lemb  34688  hgt750lema  34689  tgoldbachgtda  34693  tgoldbachgt  34695  subfacval2  35209  subfaclim  35210  bccolsum  35756  sumeq12sdv  36235  knoppndvlem6  36535  mettrifi  37781  rrncmslem  37856  sticksstones6  42164  sticksstones7  42165  sticksstones8  42166  sticksstones9  42167  sticksstones10  42168  sticksstones11  42169  sticksstones12a  42170  sticksstones12  42171  sticksstones16  42175  unitscyglem2  42209  unitscyglem4  42211  fzosumm1  42301  fz1sump1  42359  sumcubes  42362  k0004val  44174  binomcxplemnn0  44373  fsumnncl  45601  fsumiunss  45604  fsumsermpt  45608  sumnnodd  45659  dvnmul  45972  dvnprodlem3  45977  itgspltprt  46008  stoweidlem17  46046  stoweidlem20  46049  stirlinglem12  46114  dirkertrigeqlem1  46127  dirkertrigeqlem3  46129  fourierdlem83  46218  fourierdlem112  46247  fourierdlem113  46248  elaa2lem  46262  etransclem32  46295  sge00  46405  sge0iunmptlemre  46444  sge0reuzb  46477  meaiuninclem  46509  carageniuncllem1  46550  hoidmvlelem3  46626  nnsum3primes4  47802  nnsum3primesprm  47804  nnsum3primesgbe  47806  nnsum4primesodd  47810  nnsum4primesoddALTV  47811  wtgoldbnnsum4prm  47816  bgoldbnnsum3prm  47818  altgsumbcALT  48328  nn0sumshdiglemA  48599  nn0sumshdiglemB  48600  nn0sumshdiglem1  48601  nn0sumshdiglem2  48602