Theorem sumeq1d 15860

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

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

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5657  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-iota 6493  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7421  df-oprab 7422  df-mpo 7423  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-seq 14138  df-sum 15847

This theorem is used by:  sumeq12dv  15865  sumeq12rdv  15866  fsumf1o  15882  sumss  15883  fsumcllem  15891  fsumsplit1  15904  fsum1  15906  fzosump1  15911  fsump1  15915  fsum2d  15930  fsumcom2  15933  fsumshftm  15940  fsumrev2  15941  telfsumo  15962  telfsum  15964  telfsum2  15965  fsumparts  15966  fsumiun  15981  bcxmas  15997  incexclem  15998  incexc2  16000  isumsplit  16002  isum1p  16003  arisum  16022  arisum2  16023  geoser  16029  pwdif  16030  geolim  16032  geo2sum2  16036  mertenslem1  16046  mertenslem2  16047  mertens  16048  bpolydiflem  16213  efcvgfsum  16245  fprodefsum  16254  eftlub  16270  effsumlt  16272  eirrlem  16365  pwp1fsum  16554  bitsinv1  16605  bitsinvp1  16612  pcfac  17070  prmreclem4  17090  prmreclem6  17092  ovoliunlem1  25816  uniioombllem3  25899  itg11  26005  dvfsumlem1  26339  dvfsumlem4  26342  dvfsum2  26347  elplyr  26512  coeeu  26537  coeeq  26539  plyco  26553  0dgrb  26558  dvply2g  26599  vieta1lem2  26627  vieta1  26628  aaliou3lem5  26667  aaliou3lem6  26668  aaliou3lem7  26669  taylpfval  26685  pserdvlem2  26748  abelthlem6  26756  logfac  26922  advlogexp  26976  emcllem2  27317  emcllem3  27318  emcllem7  27322  harmonicbnd  27324  harmonicbnd2  27325  harmonicbnd3  27328  harmonicbnd4  27331  chtval  27430  chpval  27442  chtfl  27469  chpfl  27470  chtprm  27473  chtnprm  27474  chpp1  27475  chtdif  27478  prmorcht  27498  musum  27511  muinv  27513  logfaclbnd  27542  logfacbnd3  27543  logexprlim  27545  chtppilimlem1  27793  rplogsumlem2  27805  rpvmasumlem  27807  dchrisumlem1  27809  dchrisumlem2  27810  dchrisumlem3  27811  dchrisum  27812  dchrisum0fval  27825  dchrisum0ff  27827  dchrisum0flblem1  27828  dchrisum0lem2  27838  dchrisum0  27840  mulog2sumlem1  27854  2vmadivsumlem  27860  log2sumbnd  27864  logdivbnd  27876  selberg3lem1  27877  pntrsumbnd  27886  pntrsumbnd2  27887  pntrlog2bndlem1  27897  pntrlog2bndlem4  27900  pntpbnd1  27906  pntpbnd2  27907  pntlemf  27925  brcgr  29471  axlowdimlem16  29528  eengv  29550  finsumvtxdg2sstep  30123  eulerpartlemgs2  35005  signsvfn  35204  fsum2dsub  35229  reprval  35232  reprsuc  35237  hashrepr  35247  chpvalz  35250  chtvalz  35251  breprexplema  35252  breprexplemc  35254  breprexp  35255  breprexpnat  35256  vtsval  35259  circlemeth  35262  hgt750lemb  35278  hgt750lema  35279  tgoldbachgtda  35283  tgoldbachgt  35285  subfacval2  35931  subfaclim  35932  bccolsum  36483  sumeq12sdv  36986  knoppndvlem6  37363  mettrifi  38671  rrncmslem  38746  sticksstones6  43181  sticksstones7  43182  sticksstones8  43183  sticksstones9  43184  sticksstones10  43185  sticksstones11  43186  sticksstones12a  43187  sticksstones12  43188  sticksstones16  43192  unitscyglem2  43226  unitscyglem4  43228  fzosumm1  43281  fz1sump1  43347  sumcubes  43350  k0004val  45135  binomcxplemnn0  45318  fsumnncl  46553  fsumiunss  46556  fsumsermpt  46560  sumnnodd  46611  dvnmul  46922  dvnprodlem3  46927  itgspltprt  46958  stoweidlem17  46996  stoweidlem20  46999  stirlinglem12  47064  dirkertrigeqlem1  47077  dirkertrigeqlem3  47079  fourierdlem83  47168  fourierdlem112  47197  fourierdlem113  47198  elaa2lem  47212  etransclem32  47245  sge00  47355  sge0iunmptlemre  47394  sge0reuzb  47427  meaiuninclem  47459  carageniuncllem1  47500  hoidmvlelem3  47576  ppivalnn  48686  nnsum3primes4  48855  nnsum3primesprm  48857  nnsum3primesgbe  48859  nnsum4primesodd  48863  nnsum4primesoddALTV  48864  wtgoldbnnsum4prm  48869  bgoldbnnsum3prm  48871  altgsumbcALT  49434  nn0sumshdiglemA  49700  nn0sumshdiglemB  49701  nn0sumshdiglem1  49702  nn0sumshdiglem2  49703