Theorem sumeq1d 14431

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

Syntax hints:   → wi 4   = wceq 1483  Σcsu 14416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-xp 5120  df-cnv 5122  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-iota 5851  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-seq 12802  df-sum 14417

This theorem is referenced by:  sumeq12dv  14437  sumeq12rdv  14438  fsumf1o  14454  sumss  14455  fsumcllem  14463  fsum1  14476  fzosump1  14481  fsump1  14487  fsum2d  14502  fsumcom2  14505  fsumcom2OLD  14506  fsumshftm  14513  fsumrev2  14514  telfsumo  14534  telfsum  14536  telfsum2  14537  fsumparts  14538  fsumiun  14553  bcxmas  14567  incexclem  14568  incexc2  14570  isumsplit  14572  isum1p  14573  arisum  14592  arisum2  14593  geoser  14599  geolim  14601  geo2sum2  14605  mertenslem1  14616  mertenslem2  14617  mertens  14618  bpolydiflem  14785  efcvgfsum  14816  fprodefsum  14825  eftlub  14839  effsumlt  14841  eirrlem  14932  pwp1fsum  15114  bitsinv1  15164  bitsinvp1  15171  pcfac  15603  prmreclem4  15623  prmreclem6  15625  ovoliunlem1  23270  uniioombllem3  23353  itg11  23458  dvfsumlem1  23789  dvfsumlem4  23792  dvfsum2  23797  elplyr  23957  coeeu  23981  coeeq  23983  plyco  23997  0dgrb  24002  dvply2g  24040  vieta1lem2  24066  vieta1  24067  aaliou3lem5  24102  aaliou3lem6  24103  aaliou3lem7  24104  taylpfval  24119  pserdvlem2  24182  abelthlem6  24190  logfac  24347  advlogexp  24401  emcllem2  24723  emcllem3  24724  emcllem7  24728  harmonicbnd  24730  harmonicbnd2  24731  harmonicbnd3  24734  harmonicbnd4  24737  chtval  24836  chpval  24848  chtfl  24875  chpfl  24876  chtprm  24879  chtnprm  24880  chpp1  24881  chtdif  24884  prmorcht  24904  musum  24917  muinv  24919  logfaclbnd  24947  logfacbnd3  24948  logexprlim  24950  chtppilimlem1  25162  rplogsumlem2  25174  rpvmasumlem  25176  dchrisumlem1  25178  dchrisumlem2  25179  dchrisumlem3  25180  dchrisum  25181  dchrisum0fval  25194  dchrisum0ff  25196  dchrisum0flblem1  25197  dchrisum0lem2  25207  dchrisum0  25209  mulog2sumlem1  25223  2vmadivsumlem  25229  log2sumbnd  25233  logdivbnd  25245  selberg3lem1  25246  pntrsumbnd  25255  pntrsumbnd2  25256  pntrlog2bndlem1  25266  pntrlog2bndlem4  25269  pntpbnd1  25275  pntpbnd2  25276  pntlemf  25294  brcgr  25780  axlowdimlem16  25837  eengv  25859  finsumvtxdg2sstep  26445  eulerpartlemgs2  30442  signsvfn  30659  fsum2dsub  30685  reprval  30688  reprsuc  30693  hashrepr  30703  chpvalz  30706  chtvalz  30707  breprexplema  30708  breprexplemc  30710  breprexp  30711  breprexpnat  30712  vtsval  30715  circlemeth  30718  hgt750lemb  30734  hgt750lema  30735  tgoldbachgtda  30739  tgoldbachgt  30741  subfacval2  31169  subfaclim  31170  bccolsum  31625  knoppndvlem6  32508  mettrifi  33553  rrncmslem  33631  k0004val  38448  binomcxplemnn0  38548  fsumnncl  39803  fsumsplit1  39804  fsumiunss  39807  fsumsermpt  39811  sumnnodd  39862  dvnmul  40158  dvnprodlem3  40163  itgspltprt  40195  stoweidlem17  40234  stoweidlem20  40237  stirlinglem12  40302  dirkertrigeqlem1  40315  dirkertrigeqlem3  40317  fourierdlem83  40406  fourierdlem112  40435  fourierdlem113  40436  elaa2lem  40450  etransclem32  40483  sge00  40593  sge0iunmptlemre  40632  sge0reuzb  40665  meaiuninclem  40697  carageniuncllem1  40735  hoidmvlelem3  40811  pwdif  41501  nnsum3primes4  41676  nnsum3primesprm  41678  nnsum3primesgbe  41680  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  wtgoldbnnsum4prm  41690  bgoldbnnsum3prm  41692  altgsumbcALT  42131  nn0sumshdiglemA  42413  nn0sumshdiglemB  42414  nn0sumshdiglem1  42415  nn0sumshdiglem2  42416