Theorem sumeq2dv 15729

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1560   ∈ wcel 2142  Σcsu 15713

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-cnex 11129  ax-resscn 11130  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-mulcom 11137  ax-addass 11138  ax-mulass 11139  ax-distr 11140  ax-i2m1 11141  ax-1ne0 11142  ax-1rid 11143  ax-rnegex 11144  ax-rrecex 11145  ax-cnre 11146  ax-pre-lttri 11147  ax-pre-lttrn 11148  ax-pre-ltadd 11149  ax-pre-mulgt0 11150

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6288  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-om 7847  df-1st 7970  df-2nd 7971  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8381  df-er 8678  df-en 8928  df-dom 8929  df-sdom 8930  df-pnf 11218  df-mnf 11219  df-xr 11220  df-ltxr 11221  df-le 11222  df-sub 11416  df-neg 11417  df-nn 12211  df-n0 12482  df-z 12569  df-uz 12840  df-fz 13513  df-seq 14015  df-sum 15714

This theorem is referenced by:  2sumeq2dv  15732  sumeq12dv  15733  sumeq12rdv  15734  fsumf1o  15750  fsumss  15752  fsumsplit  15768  isummulc1  15790  isumdivc  15791  isumge0  15793  fsum2dlem  15797  fsumshftm  15808  fsum0diag2  15810  fsummulc1  15812  fsumdivc  15813  fsumneg  15814  fsumsub  15815  fsum2mul  15816  telfsumo2  15831  fsumparts  15834  hashiun  15850  hash2iun  15851  hash2iun1dif1  15852  indsum  15856  ackbijnn  15858  binomlem  15859  binom1p  15861  incexclem  15866  incexc  15867  incexc2  15868  isum1p  15871  arisum  15890  trireciplem  15892  geoserg  15896  pwdif  15898  geo2sum  15903  mertenslem1  15914  mertenslem2  15915  mertens  15916  binomfallfaclem2  16070  binomrisefac  16072  bpolylem  16078  bpolydiflem  16084  fsumkthpow  16086  efaddlem  16123  rpnnen2lem10  16255  rpnnen2lem11  16256  fsumdvds  16342  pwp1fsum  16425  phisum  16826  pcfac  16935  ramcl  17065  lagsubg2  19235  sylow2a  19659  rrxcph  25454  trirn  25462  rrxmval  25467  rrxmet  25470  ovoliunnul  25569  ovolicc2lem4  25582  uniioombllem4  25648  vitalilem5  25674  itg1addlem4  25761  itg1addlem5  25762  itg1mulc  25766  itg10a  25772  itg1climres  25776  itgss  25874  itgeqa  25876  itgsplit  25898  elply2  26256  elplyd  26262  plyeq0lem  26270  plyaddlem1  26273  plymullem1  26274  coeeulem  26284  coeeq2  26302  coemullem  26310  coe1termlem  26318  plycjlem  26336  plyrecj  26341  plyn0mulidp  26345  dvply1  26348  elqaalem3  26385  aareccl  26390  aannenlem1  26392  taylpval  26430  dvtaylp  26433  pserdvlem2  26491  pserdv2  26493  abelthlem8  26502  abelthlem9  26503  abelth  26504  logtayl  26725  leibpi  27007  birthdaylem2  27017  amgmlem  27054  emcllem5  27064  fsumharmonic  27076  lgamcvg2  27119  ftalem5  27141  basellem3  27147  basellem8  27152  sgmval2  27207  fsumdvdscom  27249  dvdsflsumcom  27252  musum  27255  musumsum  27256  muinv  27257  fsumdvdsmul  27259  sgmppw  27261  1sgmprm  27263  chtlepsi  27270  pclogsum  27279  vmasum  27280  logfac2  27281  chpval2  27282  chpchtsum  27283  logexprlim  27289  logfacrlim2  27290  perfectlem2  27294  dchrsum2  27332  sumdchr2  27334  dchrhash  27335  dchr2sum  27337  sum2dchr  27338  pcbcctr  27340  bposlem2  27349  lgsquadlem1  27444  lgsquadlem2  27445  chebbnd1lem1  27533  rplogsumlem1  27548  rplogsumlem2  27549  rpvmasumlem  27551  dchrisumlem1  27553  dchrisumlem2  27554  dchrmusum2  27558  dchrvmasumlem1  27559  dchrvmasum2lem  27560  dchrvmasum2if  27561  dchrvmasumiflem1  27565  dchrvmasumiflem2  27566  dchrisum0flblem1  27572  dchrisum0fno1  27575  rpvmasum2  27576  dchrisum0lem2a  27581  dchrisum0lem2  27582  dchrisum0lem3  27583  dchrisum0  27584  rplogsum  27591  mudivsum  27594  mulogsumlem  27595  mulogsum  27596  mulog2sumlem1  27598  mulog2sumlem2  27599  mulog2sumlem3  27600  vmalogdivsum2  27602  vmalogdivsum  27603  2vmadivsumlem  27604  logsqvma  27606  logsqvma2  27607  selberglem1  27609  selberglem2  27610  selberg  27612  selberg2  27615  selberg3lem1  27621  selberg4lem1  27624  selberg4  27625  pntrsumo1  27629  selbergr  27632  selberg3r  27633  selberg4r  27634  selberg34r  27635  pntsval2  27640  pntrlog2bndlem4  27644  pntrlog2bndlem5  27645  pntpbnd1  27650  pntlemk  27670  pntlemo  27671  axcgrrflx  29115  axcgrid  29117  axsegconlem1  29118  axsegconlem9  29126  ax5seglem1  29129  ax5seglem2  29130  ax5seglem9  29138  axlowdimlem16  29158  axlowdimlem17  29159  ecgrtg  29184  finsumvtxdg2ssteplem3  29748  rusgrnumwwlks  30177  fusgrhashclwwlkn  30281  fusgreghash2wsp  30540  numclwwlk6  30592  indsumin  33039  elrgspnlem2  33424  vietadeg1  33875  eulerpartlemsv1  34653  eulerpartlemsf  34656  eulerpartlemgs2  34677  eulerpartlemn  34678  signsvfn  34876  fsum2dsub  34901  reprsuc  34909  hashreprin  34914  reprpmtf1o  34920  breprexplema  34924  breprexplemc  34926  breprexp  34927  breprexpnat  34928  vtsprod  34933  circlemeth  34934  circlemethnat  34935  circlevma  34936  circlemethhgt  34937  hgt750lemd  34942  hgt750lemb  34950  hgt750lema  34951  subfaclim  35538  fwddifnp1  36515  knoppndvlem6  36955  rrnmet  38328  3factsumint2  42639  3factsumint3  42640  lcmineqlem1  42646  lcmineqlem3  42648  lcmineqlem6  42651  sticksstones8  42770  sticksstones9  42771  sticksstones10  42772  sticksstones11  42773  sticksstones12a  42774  sticksstones12  42775  sticksstones17  42780  sticksstones18  42781  sticksstones19  42782  aks6d1c6lem1  42787  aks6d1c6lem3  42789  aks6d1c7lem3  42799  unitscyglem2  42813  sumcubes  42922  fltnltalem  43244  jm2.22  43572  jm2.23  43573  flcidc  43747  binomcxplemnn0  44925  binomcxplemdvsum  44931  binomcxplemnotnn0  44932  mccllem  46173  isumneg  46178  sumnnodd  46206  dvnmul  46517  dvnprodlem2  46521  dvnprodlem3  46522  stoweidlem37  46611  dirkertrigeqlem2  46673  dirkertrigeqlem3  46674  fourierdlem81  46761  fourierdlem83  46763  fourierdlem93  46773  fourierdlem103  46783  fourierdlem104  46784  elaa2lem  46807  etransclem23  46831  etransclem24  46832  etransclem31  46839  etransclem32  46840  etransclem35  46843  etransclem46  46854  rrxtopnfi  46861  rrndistlt  46864  sge0z  46949  sge0fsummpt  46964  sge0sup  46965  sge0resplit  46980  sge0split  46983  sge0ltfirpmpt2  47000  omeiunltfirp  47093  carageniuncllem2  47096  hoidmvlelem2  47170  hoidmvlelem3  47171  ppivalnn  48241  perfectALTVlem2  48344  nnsum3primesprm  48412  nnsum3primesgbe  48414  nnsum4primeseven  48422  altgsumbc  48974  altgsumbcALT  48975  nn0sumshdiglemA  49241  nn0sumshdiglemB  49242  nn0sumshdig  49245  aacllem  50422  amgmwlem  50423