Theorem sumeq1d 15787

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  Σcsu 15773

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-xp 5661  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-iota 6489  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7416  df-oprab 7417  df-mpo 7418  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-seq 14066  df-sum 15774

This theorem is used by:  sumeq12dv  15792  sumeq12rdv  15793  fsumf1o  15809  sumss  15810  fsumcllem  15818  fsumsplit1  15831  fsum1  15833  fzosump1  15838  fsump1  15842  fsum2d  15857  fsumcom2  15860  fsumshftm  15867  fsumrev2  15868  telfsumo  15889  telfsum  15891  telfsum2  15892  fsumparts  15893  fsumiun  15908  bcxmas  15924  incexclem  15925  incexc2  15927  isumsplit  15929  isum1p  15930  arisum  15949  arisum2  15950  geoser  15956  pwdif  15957  geolim  15959  geo2sum2  15963  mertenslem1  15973  mertenslem2  15974  mertens  15975  bpolydiflem  16140  efcvgfsum  16172  fprodefsum  16181  eftlub  16197  effsumlt  16199  eirrlem  16292  pwp1fsum  16481  bitsinv1  16532  bitsinvp1  16539  pcfac  16991  prmreclem4  17011  prmreclem6  17013  ovoliunlem1  25730  uniioombllem3  25813  itg11  25919  dvfsumlem1  26253  dvfsumlem4  26256  dvfsum2  26261  elplyr  26426  coeeu  26451  coeeq  26453  plyco  26467  0dgrb  26472  dvply2g  26515  vieta1lem2  26543  vieta1  26544  aaliou3lem5  26583  aaliou3lem6  26584  aaliou3lem7  26585  taylpfval  26601  pserdvlem2  26664  abelthlem6  26672  logfac  26838  advlogexp  26892  emcllem2  27233  emcllem3  27234  emcllem7  27238  harmonicbnd  27240  harmonicbnd2  27241  harmonicbnd3  27244  harmonicbnd4  27247  chtval  27346  chpval  27358  chtfl  27385  chpfl  27386  chtprm  27389  chtnprm  27390  chpp1  27391  chtdif  27394  prmorcht  27414  musum  27427  muinv  27429  logfaclbnd  27458  logfacbnd3  27459  logexprlim  27461  chtppilimlem1  27709  rplogsumlem2  27721  rpvmasumlem  27723  dchrisumlem1  27725  dchrisumlem2  27726  dchrisumlem3  27727  dchrisum  27728  dchrisum0fval  27741  dchrisum0ff  27743  dchrisum0flblem1  27744  dchrisum0lem2  27754  dchrisum0  27756  mulog2sumlem1  27770  2vmadivsumlem  27776  log2sumbnd  27780  logdivbnd  27792  selberg3lem1  27793  pntrsumbnd  27802  pntrsumbnd2  27803  pntrlog2bndlem1  27813  pntrlog2bndlem4  27816  pntpbnd1  27822  pntpbnd2  27823  pntlemf  27841  brcgr  29357  axlowdimlem16  29414  eengv  29436  finsumvtxdg2sstep  30009  eulerpartlemgs2  34891  signsvfn  35090  fsum2dsub  35115  reprval  35118  reprsuc  35123  hashrepr  35133  chpvalz  35136  chtvalz  35137  breprexplema  35138  breprexplemc  35140  breprexp  35141  breprexpnat  35142  vtsval  35145  circlemeth  35148  hgt750lemb  35164  hgt750lema  35165  tgoldbachgtda  35169  tgoldbachgt  35171  subfacval2  35766  subfaclim  35767  bccolsum  36318  sumeq12sdv  36837  knoppndvlem6  37214  mettrifi  38507  rrncmslem  38582  sticksstones6  43017  sticksstones7  43018  sticksstones8  43019  sticksstones9  43020  sticksstones10  43021  sticksstones11  43022  sticksstones12a  43023  sticksstones12  43024  sticksstones16  43028  unitscyglem2  43062  unitscyglem4  43064  fzosumm1  43117  fz1sump1  43185  sumcubes  43188  k0004val  44990  binomcxplemnn0  45173  fsumnncl  46402  fsumiunss  46405  fsumsermpt  46409  sumnnodd  46460  dvnmul  46771  dvnprodlem3  46776  itgspltprt  46807  stoweidlem17  46845  stoweidlem20  46848  stirlinglem12  46913  dirkertrigeqlem1  46926  dirkertrigeqlem3  46928  fourierdlem83  47017  fourierdlem112  47046  fourierdlem113  47047  elaa2lem  47061  etransclem32  47094  sge00  47204  sge0iunmptlemre  47243  sge0reuzb  47276  meaiuninclem  47308  carageniuncllem1  47349  hoidmvlelem3  47425  ppivalnn  48535  nnsum3primes4  48704  nnsum3primesprm  48706  nnsum3primesgbe  48708  nnsum4primesodd  48712  nnsum4primesoddALTV  48713  wtgoldbnnsum4prm  48718  bgoldbnnsum3prm  48720  altgsumbcALT  49283  nn0sumshdiglemA  49549  nn0sumshdiglemB  49550  nn0sumshdiglem1  49551  nn0sumshdiglem2  49552