Theorem sumeq2dv 14811

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 3176	. 2 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 = 𝐶)
3	2	sumeq2d 14810	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   ∧ wa 386   = wceq 1658   ∈ wcel 2166  Σcsu 14794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804  ax-sep 5006  ax-nul 5014  ax-pow 5066  ax-pr 5128  ax-un 7210  ax-cnex 10309  ax-resscn 10310  ax-1cn 10311  ax-icn 10312  ax-addcl 10313  ax-addrcl 10314  ax-mulcl 10315  ax-mulrcl 10316  ax-mulcom 10317  ax-addass 10318  ax-mulass 10319  ax-distr 10320  ax-i2m1 10321  ax-1ne0 10322  ax-1rid 10323  ax-rnegex 10324  ax-rrecex 10325  ax-cnre 10326  ax-pre-lttri 10327  ax-pre-lttrn 10328  ax-pre-ltadd 10329  ax-pre-mulgt0 10330

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-fal 1672  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2606  df-eu 2641  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-ne 3001  df-nel 3104  df-ral 3123  df-rex 3124  df-reu 3125  df-rab 3127  df-v 3417  df-sbc 3664  df-csb 3759  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-pss 3815  df-nul 4146  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4660  df-iun 4743  df-br 4875  df-opab 4937  df-mpt 4954  df-tr 4977  df-id 5251  df-eprel 5256  df-po 5264  df-so 5265  df-fr 5302  df-we 5304  df-xp 5349  df-rel 5350  df-cnv 5351  df-co 5352  df-dm 5353  df-rn 5354  df-res 5355  df-ima 5356  df-pred 5921  df-ord 5967  df-on 5968  df-lim 5969  df-suc 5970  df-iota 6087  df-fun 6126  df-fn 6127  df-f 6128  df-f1 6129  df-fo 6130  df-f1o 6131  df-fv 6132  df-riota 6867  df-ov 6909  df-oprab 6910  df-mpt2 6911  df-om 7328  df-1st 7429  df-2nd 7430  df-wrecs 7673  df-recs 7735  df-rdg 7773  df-er 8010  df-en 8224  df-dom 8225  df-sdom 8226  df-pnf 10394  df-mnf 10395  df-xr 10396  df-ltxr 10397  df-le 10398  df-sub 10588  df-neg 10589  df-nn 11352  df-n0 11620  df-z 11706  df-uz 11970  df-fz 12621  df-seq 13097  df-sum 14795

This theorem is referenced by:  sumeq2sdv  14813  2sumeq2dv  14814  sumeq12dv  14815  sumeq12rdv  14816  fsumf1o  14832  fsumss  14834  fsumsplit  14849  isummulc1  14870  isumdivc  14871  isumge0  14873  fsum2dlem  14877  fsumshftm  14888  fsum0diag2  14890  fsummulc1  14892  fsumdivc  14893  fsumneg  14894  fsumsub  14895  fsum2mul  14896  telfsumo2  14910  fsumparts  14913  hashiun  14929  hash2iun  14930  hash2iun1dif1  14931  ackbijnn  14935  binomlem  14936  binom1p  14938  incexclem  14943  incexc  14944  incexc2  14945  isum1p  14948  arisum  14967  trireciplem  14969  geoserg  14973  geo2sum  14979  mertenslem1  14990  mertenslem2  14991  mertens  14992  binomfallfaclem2  15144  binomrisefac  15146  bpolylem  15152  bpolydiflem  15158  fsumkthpow  15160  efaddlem  15196  rpnnen2lem10  15327  rpnnen2lem11  15328  fsumdvds  15408  pwp1fsum  15489  phisum  15867  pcfac  15975  ramcl  16105  lagsubg2  18007  sylow2a  18386  rrxcph  23561  trirn  23569  rrxmval  23574  rrxmet  23577  ovoliunnul  23674  ovolicc2lem4  23687  uniioombllem4  23753  vitalilem5  23779  itg1addlem4  23866  itg1addlem5  23867  itg1mulc  23871  itg10a  23877  itg1climres  23881  itgss  23978  itgeqa  23980  itgsplit  24002  elply2  24352  elplyd  24358  plyeq0lem  24366  plyaddlem1  24369  plymullem1  24370  coeeulem  24380  coeeq2  24398  coemullem  24406  coe1termlem  24414  plycjlem  24432  plyrecj  24435  dvply1  24439  elqaalem3  24476  aareccl  24481  aannenlem1  24483  taylpval  24521  dvtaylp  24524  pserdvlem2  24582  pserdv2  24584  abelthlem8  24593  abelthlem9  24594  abelth  24595  logtayl  24806  leibpi  25083  birthdaylem2  25093  amgmlem  25130  emcllem5  25140  fsumharmonic  25152  lgamcvg2  25195  ftalem5  25217  basellem3  25223  basellem8  25228  sgmval2  25283  fsumdvdscom  25325  dvdsflsumcom  25328  musum  25331  musumsum  25332  muinv  25333  fsumdvdsmul  25335  sgmppw  25336  1sgmprm  25338  chtlepsi  25345  pclogsum  25354  vmasum  25355  logfac2  25356  chpval2  25357  chpchtsum  25358  logexprlim  25364  logfacrlim2  25365  perfectlem2  25369  dchrsum2  25407  sumdchr2  25409  dchrhash  25410  dchr2sum  25412  sum2dchr  25413  pcbcctr  25415  bposlem2  25424  lgsquadlem1  25519  lgsquadlem2  25520  chebbnd1lem1  25572  rplogsumlem1  25587  rplogsumlem2  25588  rpvmasumlem  25590  dchrisumlem1  25592  dchrisumlem2  25593  dchrmusum2  25597  dchrvmasumlem1  25598  dchrvmasum2lem  25599  dchrvmasum2if  25600  dchrvmasumiflem1  25604  dchrvmasumiflem2  25605  dchrisum0flblem1  25611  dchrisum0fno1  25614  rpvmasum2  25615  dchrisum0lem2a  25620  dchrisum0lem2  25621  dchrisum0lem3  25622  dchrisum0  25623  rplogsum  25630  mudivsum  25633  mulogsumlem  25634  mulogsum  25635  mulog2sumlem1  25637  mulog2sumlem2  25638  mulog2sumlem3  25639  vmalogdivsum2  25641  vmalogdivsum  25642  2vmadivsumlem  25643  logsqvma  25645  logsqvma2  25646  selberglem1  25648  selberglem2  25649  selberg  25651  selberg2  25654  selberg3lem1  25660  selberg4lem1  25663  selberg4  25664  pntrsumo1  25668  selbergr  25671  selberg3r  25672  selberg4r  25673  selberg34r  25674  pntsval2  25679  pntrlog2bndlem4  25683  pntrlog2bndlem5  25684  pntpbnd1  25689  pntlemk  25709  pntlemo  25710  axcgrrflx  26214  axcgrid  26216  axsegconlem1  26217  axsegconlem9  26225  ax5seglem1  26228  ax5seglem2  26229  ax5seglem9  26237  axlowdimlem16  26257  axlowdimlem17  26258  ecgrtg  26283  finsumvtxdg2ssteplem3  26846  rusgrnumwwlks  27304  rusgrnumwwlksOLD  27305  fusgrhashclwwlkn  27433  fusgreghash2wsp  27720  numclwwlk6  27806  indsum  30629  indsumin  30630  eulerpartlemsv1  30964  eulerpartlemsf  30967  eulerpartlemgs2  30988  eulerpartlemn  30989  plymulx0  31172  signsvfn  31209  fsum2dsub  31235  reprsuc  31243  hashreprin  31248  reprpmtf1o  31254  breprexplema  31258  breprexplemc  31260  breprexp  31261  breprexpnat  31262  vtsprod  31267  circlemeth  31268  circlemethnat  31269  circlevma  31270  circlemethhgt  31271  hgt750lemd  31276  hgt750lemb  31284  hgt750lema  31285  subfaclim  31717  fwddifnp1  32812  knoppndvlem6  33041  rrnmet  34171  jm2.22  38406  jm2.23  38407  flcidc  38588  binomcxplemnn0  39389  binomcxplemdvsum  39395  binomcxplemnotnn0  39396  mccllem  40625  isumneg  40630  sumnnodd  40658  dvnmul  40954  dvnprodlem2  40958  dvnprodlem3  40959  stoweidlem37  41049  dirkertrigeqlem2  41111  dirkertrigeqlem3  41112  fourierdlem81  41199  fourierdlem83  41201  fourierdlem93  41211  fourierdlem103  41221  fourierdlem104  41222  elaa2lem  41245  etransclem23  41269  etransclem24  41270  etransclem31  41277  etransclem32  41278  etransclem35  41281  etransclem46  41292  rrxtopnfi  41299  rrndistlt  41302  sge0z  41384  sge0fsummpt  41399  sge0sup  41400  sge0resplit  41415  sge0split  41418  sge0ltfirpmpt2  41435  omeiunltfirp  41528  carageniuncllem2  41531  hoidmvlelem2  41605  hoidmvlelem3  41606  pwdif  42332  perfectALTVlem2  42462  nnsum3primesprm  42509  nnsum3primesgbe  42511  nnsum4primeseven  42519  altgsumbc  42978  altgsumbcALT  42979  nn0sumshdiglemA  43261  nn0sumshdiglemB  43262  nn0sumshdig  43265  aacllem  43444  amgmwlem  43445