Theorem sumeq2dv 15738

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

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

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-n0 12527  df-z 12614  df-uz 12879  df-fz 13548  df-seq 14043  df-sum 15723

This theorem is referenced by:  2sumeq2dv  15741  sumeq12dv  15742  sumeq12rdv  15743  fsumf1o  15759  fsumss  15761  fsumsplit  15777  isummulc1  15799  isumdivc  15800  isumge0  15802  fsum2dlem  15806  fsumshftm  15817  fsum0diag2  15819  fsummulc1  15821  fsumdivc  15822  fsumneg  15823  fsumsub  15824  fsum2mul  15825  telfsumo2  15839  fsumparts  15842  hashiun  15858  hash2iun  15859  hash2iun1dif1  15860  ackbijnn  15864  binomlem  15865  binom1p  15867  incexclem  15872  incexc  15873  incexc2  15874  isum1p  15877  arisum  15896  trireciplem  15898  geoserg  15902  pwdif  15904  geo2sum  15909  mertenslem1  15920  mertenslem2  15921  mertens  15922  binomfallfaclem2  16076  binomrisefac  16078  bpolylem  16084  bpolydiflem  16090  fsumkthpow  16092  efaddlem  16129  rpnnen2lem10  16259  rpnnen2lem11  16260  fsumdvds  16345  pwp1fsum  16428  phisum  16828  pcfac  16937  ramcl  17067  lagsubg2  19212  sylow2a  19637  rrxcph  25426  trirn  25434  rrxmval  25439  rrxmet  25442  ovoliunnul  25542  ovolicc2lem4  25555  uniioombllem4  25621  vitalilem5  25647  itg1addlem4  25734  itg1addlem5  25735  itg1mulc  25739  itg10a  25745  itg1climres  25749  itgss  25847  itgeqa  25849  itgsplit  25871  elply2  26235  elplyd  26241  plyeq0lem  26249  plyaddlem1  26252  plymullem1  26253  coeeulem  26263  coeeq2  26281  coemullem  26289  coe1termlem  26297  plycjlem  26316  plyrecj  26321  dvply1  26325  elqaalem3  26363  aareccl  26368  aannenlem1  26370  taylpval  26408  dvtaylp  26412  pserdvlem2  26472  pserdv2  26474  abelthlem8  26483  abelthlem9  26484  abelth  26485  logtayl  26702  leibpi  26985  birthdaylem2  26995  amgmlem  27033  emcllem5  27043  fsumharmonic  27055  lgamcvg2  27098  ftalem5  27120  basellem3  27126  basellem8  27131  sgmval2  27186  fsumdvdscom  27228  dvdsflsumcom  27231  musum  27234  musumsum  27235  muinv  27236  fsumdvdsmul  27238  fsumdvdsmulOLD  27240  sgmppw  27241  1sgmprm  27243  chtlepsi  27250  pclogsum  27259  vmasum  27260  logfac2  27261  chpval2  27262  chpchtsum  27263  logexprlim  27269  logfacrlim2  27270  perfectlem2  27274  dchrsum2  27312  sumdchr2  27314  dchrhash  27315  dchr2sum  27317  sum2dchr  27318  pcbcctr  27320  bposlem2  27329  lgsquadlem1  27424  lgsquadlem2  27425  chebbnd1lem1  27513  rplogsumlem1  27528  rplogsumlem2  27529  rpvmasumlem  27531  dchrisumlem1  27533  dchrisumlem2  27534  dchrmusum2  27538  dchrvmasumlem1  27539  dchrvmasum2lem  27540  dchrvmasum2if  27541  dchrvmasumiflem1  27545  dchrvmasumiflem2  27546  dchrisum0flblem1  27552  dchrisum0fno1  27555  rpvmasum2  27556  dchrisum0lem2a  27561  dchrisum0lem2  27562  dchrisum0lem3  27563  dchrisum0  27564  rplogsum  27571  mudivsum  27574  mulogsumlem  27575  mulogsum  27576  mulog2sumlem1  27578  mulog2sumlem2  27579  mulog2sumlem3  27580  vmalogdivsum2  27582  vmalogdivsum  27583  2vmadivsumlem  27584  logsqvma  27586  logsqvma2  27587  selberglem1  27589  selberglem2  27590  selberg  27592  selberg2  27595  selberg3lem1  27601  selberg4lem1  27604  selberg4  27605  pntrsumo1  27609  selbergr  27612  selberg3r  27613  selberg4r  27614  selberg34r  27615  pntsval2  27620  pntrlog2bndlem4  27624  pntrlog2bndlem5  27625  pntpbnd1  27630  pntlemk  27650  pntlemo  27651  axcgrrflx  28929  axcgrid  28931  axsegconlem1  28932  axsegconlem9  28940  ax5seglem1  28943  ax5seglem2  28944  ax5seglem9  28952  axlowdimlem16  28972  axlowdimlem17  28973  ecgrtg  28998  finsumvtxdg2ssteplem3  29565  rusgrnumwwlks  29994  fusgrhashclwwlkn  30098  fusgreghash2wsp  30357  numclwwlk6  30409  indsum  32846  indsumin  32847  elrgspnlem2  33247  eulerpartlemsv1  34358  eulerpartlemsf  34361  eulerpartlemgs2  34382  eulerpartlemn  34383  plymulx0  34562  signsvfn  34597  fsum2dsub  34622  reprsuc  34630  hashreprin  34635  reprpmtf1o  34641  breprexplema  34645  breprexplemc  34647  breprexp  34648  breprexpnat  34649  vtsprod  34654  circlemeth  34655  circlemethnat  34656  circlevma  34657  circlemethhgt  34658  hgt750lemd  34663  hgt750lemb  34671  hgt750lema  34672  subfaclim  35193  fwddifnp1  36166  knoppndvlem6  36518  rrnmet  37836  3factsumint2  42023  3factsumint3  42024  lcmineqlem1  42030  lcmineqlem3  42032  lcmineqlem6  42035  sticksstones8  42154  sticksstones9  42155  sticksstones10  42156  sticksstones11  42157  sticksstones12a  42158  sticksstones12  42159  sticksstones17  42164  sticksstones18  42165  sticksstones19  42166  aks6d1c6lem1  42171  aks6d1c6lem3  42173  aks6d1c7lem3  42183  unitscyglem2  42197  sumcubes  42347  fltnltalem  42672  jm2.22  43007  jm2.23  43008  flcidc  43182  binomcxplemnn0  44368  binomcxplemdvsum  44374  binomcxplemnotnn0  44375  mccllem  45612  isumneg  45617  sumnnodd  45645  dvnmul  45958  dvnprodlem2  45962  dvnprodlem3  45963  stoweidlem37  46052  dirkertrigeqlem2  46114  dirkertrigeqlem3  46115  fourierdlem81  46202  fourierdlem83  46204  fourierdlem93  46214  fourierdlem103  46224  fourierdlem104  46225  elaa2lem  46248  etransclem23  46272  etransclem24  46273  etransclem31  46280  etransclem32  46281  etransclem35  46284  etransclem46  46295  rrxtopnfi  46302  rrndistlt  46305  sge0z  46390  sge0fsummpt  46405  sge0sup  46406  sge0resplit  46421  sge0split  46424  sge0ltfirpmpt2  46441  omeiunltfirp  46534  carageniuncllem2  46537  hoidmvlelem2  46611  hoidmvlelem3  46612  perfectALTVlem2  47709  nnsum3primesprm  47777  nnsum3primesgbe  47779  nnsum4primeseven  47787  altgsumbc  48268  altgsumbcALT  48269  nn0sumshdiglemA  48540  nn0sumshdiglemB  48541  nn0sumshdig  48544  aacllem  49320  amgmwlem  49321