Theorem sumeq2dv 15609

Description: Equality deduction for sum. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2014.)

Hypothesis

Ref	Expression
sumeq2dv.1	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 = 𝐶)

Assertion

Ref	Expression
sumeq2dv	⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶)

Distinct variable groups:   𝐴,𝑘   𝜑,𝑘

Allowed substitution hints:   𝐵(𝑘)   𝐶(𝑘)

Proof of Theorem sumeq2dv

Step	Hyp	Ref	Expression
1		sumeq2dv.1	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 = 𝐶)
2	1	ralrimiva 3121	. 2 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 = 𝐶)
3	2	sumeq2d 15608	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Σcsu 15593

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-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-om 7800  df-1st 7924  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-sub 11349  df-neg 11350  df-nn 12129  df-n0 12385  df-z 12472  df-uz 12736  df-fz 13411  df-seq 13909  df-sum 15594

This theorem is referenced by:  2sumeq2dv  15612  sumeq12dv  15613  sumeq12rdv  15614  fsumf1o  15630  fsumss  15632  fsumsplit  15648  isummulc1  15670  isumdivc  15671  isumge0  15673  fsum2dlem  15677  fsumshftm  15688  fsum0diag2  15690  fsummulc1  15692  fsumdivc  15693  fsumneg  15694  fsumsub  15695  fsum2mul  15696  telfsumo2  15710  fsumparts  15713  hashiun  15729  hash2iun  15730  hash2iun1dif1  15731  ackbijnn  15735  binomlem  15736  binom1p  15738  incexclem  15743  incexc  15744  incexc2  15745  isum1p  15748  arisum  15767  trireciplem  15769  geoserg  15773  pwdif  15775  geo2sum  15780  mertenslem1  15791  mertenslem2  15792  mertens  15793  binomfallfaclem2  15947  binomrisefac  15949  bpolylem  15955  bpolydiflem  15961  fsumkthpow  15963  efaddlem  16000  rpnnen2lem10  16132  rpnnen2lem11  16133  fsumdvds  16219  pwp1fsum  16302  phisum  16702  pcfac  16811  ramcl  16941  lagsubg2  19073  sylow2a  19498  rrxcph  25290  trirn  25298  rrxmval  25303  rrxmet  25306  ovoliunnul  25406  ovolicc2lem4  25419  uniioombllem4  25485  vitalilem5  25511  itg1addlem4  25598  itg1addlem5  25599  itg1mulc  25603  itg10a  25609  itg1climres  25613  itgss  25711  itgeqa  25713  itgsplit  25735  elply2  26099  elplyd  26105  plyeq0lem  26113  plyaddlem1  26116  plymullem1  26117  coeeulem  26127  coeeq2  26145  coemullem  26153  coe1termlem  26161  plycjlem  26180  plyrecj  26185  dvply1  26189  elqaalem3  26227  aareccl  26232  aannenlem1  26234  taylpval  26272  dvtaylp  26276  pserdvlem2  26336  pserdv2  26338  abelthlem8  26347  abelthlem9  26348  abelth  26349  logtayl  26567  leibpi  26850  birthdaylem2  26860  amgmlem  26898  emcllem5  26908  fsumharmonic  26920  lgamcvg2  26963  ftalem5  26985  basellem3  26991  basellem8  26996  sgmval2  27051  fsumdvdscom  27093  dvdsflsumcom  27096  musum  27099  musumsum  27100  muinv  27101  fsumdvdsmul  27103  fsumdvdsmulOLD  27105  sgmppw  27106  1sgmprm  27108  chtlepsi  27115  pclogsum  27124  vmasum  27125  logfac2  27126  chpval2  27127  chpchtsum  27128  logexprlim  27134  logfacrlim2  27135  perfectlem2  27139  dchrsum2  27177  sumdchr2  27179  dchrhash  27180  dchr2sum  27182  sum2dchr  27183  pcbcctr  27185  bposlem2  27194  lgsquadlem1  27289  lgsquadlem2  27290  chebbnd1lem1  27378  rplogsumlem1  27393  rplogsumlem2  27394  rpvmasumlem  27396  dchrisumlem1  27398  dchrisumlem2  27399  dchrmusum2  27403  dchrvmasumlem1  27404  dchrvmasum2lem  27405  dchrvmasum2if  27406  dchrvmasumiflem1  27410  dchrvmasumiflem2  27411  dchrisum0flblem1  27417  dchrisum0fno1  27420  rpvmasum2  27421  dchrisum0lem2a  27426  dchrisum0lem2  27427  dchrisum0lem3  27428  dchrisum0  27429  rplogsum  27436  mudivsum  27439  mulogsumlem  27440  mulogsum  27441  mulog2sumlem1  27443  mulog2sumlem2  27444  mulog2sumlem3  27445  vmalogdivsum2  27447  vmalogdivsum  27448  2vmadivsumlem  27449  logsqvma  27451  logsqvma2  27452  selberglem1  27454  selberglem2  27455  selberg  27457  selberg2  27460  selberg3lem1  27466  selberg4lem1  27469  selberg4  27470  pntrsumo1  27474  selbergr  27477  selberg3r  27478  selberg4r  27479  selberg34r  27480  pntsval2  27485  pntrlog2bndlem4  27489  pntrlog2bndlem5  27490  pntpbnd1  27495  pntlemk  27515  pntlemo  27516  axcgrrflx  28859  axcgrid  28861  axsegconlem1  28862  axsegconlem9  28870  ax5seglem1  28873  ax5seglem2  28874  ax5seglem9  28882  axlowdimlem16  28902  axlowdimlem17  28903  ecgrtg  28928  finsumvtxdg2ssteplem3  29493  rusgrnumwwlks  29919  fusgrhashclwwlkn  30023  fusgreghash2wsp  30282  numclwwlk6  30334  indsum  32804  indsumin  32805  elrgspnlem2  33183  eulerpartlemsv1  34324  eulerpartlemsf  34327  eulerpartlemgs2  34348  eulerpartlemn  34349  plymulx0  34515  signsvfn  34550  fsum2dsub  34575  reprsuc  34583  hashreprin  34588  reprpmtf1o  34594  breprexplema  34598  breprexplemc  34600  breprexp  34601  breprexpnat  34602  vtsprod  34607  circlemeth  34608  circlemethnat  34609  circlevma  34610  circlemethhgt  34611  hgt750lemd  34616  hgt750lemb  34624  hgt750lema  34625  subfaclim  35165  fwddifnp1  36143  knoppndvlem6  36495  rrnmet  37813  3factsumint2  41999  3factsumint3  42000  lcmineqlem1  42006  lcmineqlem3  42008  lcmineqlem6  42011  sticksstones8  42130  sticksstones9  42131  sticksstones10  42132  sticksstones11  42133  sticksstones12a  42134  sticksstones12  42135  sticksstones17  42140  sticksstones18  42141  sticksstones19  42142  aks6d1c6lem1  42147  aks6d1c6lem3  42149  aks6d1c7lem3  42159  unitscyglem2  42173  sumcubes  42290  fltnltalem  42639  jm2.22  42972  jm2.23  42973  flcidc  43147  binomcxplemnn0  44326  binomcxplemdvsum  44332  binomcxplemnotnn0  44333  mccllem  45582  isumneg  45587  sumnnodd  45615  dvnmul  45928  dvnprodlem2  45932  dvnprodlem3  45933  stoweidlem37  46022  dirkertrigeqlem2  46084  dirkertrigeqlem3  46085  fourierdlem81  46172  fourierdlem83  46174  fourierdlem93  46184  fourierdlem103  46194  fourierdlem104  46195  elaa2lem  46218  etransclem23  46242  etransclem24  46243  etransclem31  46250  etransclem32  46251  etransclem35  46254  etransclem46  46265  rrxtopnfi  46272  rrndistlt  46275  sge0z  46360  sge0fsummpt  46375  sge0sup  46376  sge0resplit  46391  sge0split  46394  sge0ltfirpmpt2  46411  omeiunltfirp  46504  carageniuncllem2  46507  hoidmvlelem2  46581  hoidmvlelem3  46582  perfectALTVlem2  47710  nnsum3primesprm  47778  nnsum3primesgbe  47780  nnsum4primeseven  47788  altgsumbc  48340  altgsumbcALT  48341  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  nn0sumshdig  48612  aacllem  49790  amgmwlem  49791