Theorem seqeq3d 13918

Description: Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.)

Hypothesis

Ref	Expression
seqeqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
seqeq3d	⊢ (𝜑 → seq𝑀( + , 𝐴) = seq𝑀( + , 𝐵))

Proof of Theorem seqeq3d

Step	Hyp	Ref	Expression
1		seqeqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		seqeq3 13915	. 2 ⊢ (𝐴 = 𝐵 → seq𝑀( + , 𝐴) = seq𝑀( + , 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → seq𝑀( + , 𝐴) = seq𝑀( + , 𝐵))

Syntax hints:   → wi 4   = wceq 1541  seqcseq 13910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-xp 5625  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6253  df-iota 6442  df-fv 6494  df-ov 7355  df-oprab 7356  df-mpo 7357  df-frecs 8217  df-wrecs 8248  df-recs 8297  df-rdg 8335  df-seq 13911

This theorem is referenced by:  seqeq123d  13919  seqf1olem2  13951  seqf1o  13952  seqof2  13969  expval  13972  relexp1g  14935  sumeq1  15598  sumeq2w  15601  cbvsum  15604  cbvsumv  15605  sumeq2sdv  15612  summo  15626  fsum  15629  geomulcvg  15785  prodeq1f  15815  prodeq1  15816  prodeq2w  15819  prodeq2sdv  15832  prodmo  15845  fprod  15850  gsumvalx  18586  mulgval  18986  gsumval3eu  19818  gsumval3lem2  19820  gsumzres  19823  gsumzf1o  19826  elovolmr  25405  ovolctb  25419  ovoliunlem3  25433  ovoliunnul  25436  ovolshftlem1  25438  voliunlem3  25481  voliun  25483  uniioombllem2  25512  vitalilem4  25540  vitalilem5  25541  dvnfval  25852  mtestbdd  26342  radcnv0  26353  radcnvlt1  26355  radcnvle  26357  psercn  26364  pserdvlem2  26366  abelthlem1  26369  abelthlem3  26371  logtayl  26597  atantayl2  26876  atantayl3  26877  lgamgulm2  26974  lgamcvglem  26978  lgsval  27240  lgsval4  27256  lgsneg  27260  lgsmod  27262  dchrmusumlema  27432  dchrisum0lema  27453  faclim  35811  prodeq12sdv  36283  cbvsumdavw  36344  cbvproddavw  36345  cbvsumdavw2  36360  cbvproddavw2  36361  knoppcnlem9  36566  knoppndvlem4  36580  ovoliunnfl  37722  voliunnfl  37724  radcnvrat  44431  dvradcnv2  44464  binomcxplemcvg  44471  binomcxplemdvsum  44472  binomcxplemnotnn0  44473  sumnnodd  45754  stirlinglem5  46200  sge0isummpt2  46554  ovolval2lem  46765