Theorem seqeq3d 13962

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 13959	. 2 ⊢ (𝐴 = 𝐵 → seq𝑀( + , 𝐴) = seq𝑀( + , 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → seq𝑀( + , 𝐴) = seq𝑀( + , 𝐵))

Syntax hints:   → wi 4   = wceq 1542  seqcseq 13954

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-xp 5630  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-iota 6448  df-fv 6500  df-ov 7363  df-oprab 7364  df-mpo 7365  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-seq 13955

This theorem is referenced by:  seqeq123d  13963  seqf1olem2  13995  seqf1o  13996  seqof2  14013  expval  14016  relexp1g  14979  sumeq1  15642  sumeq2w  15645  cbvsum  15648  cbvsumv  15649  sumeq2sdv  15656  summo  15670  fsum  15673  geomulcvg  15832  prodeq1f  15862  prodeq1  15863  prodeq2w  15866  prodeq2sdv  15879  prodmo  15892  fprod  15897  gsumvalx  18635  mulgval  19038  gsumval3eu  19870  gsumval3lem2  19872  gsumzres  19875  gsumzf1o  19878  elovolmr  25453  ovolctb  25467  ovoliunlem3  25481  ovoliunnul  25484  ovolshftlem1  25486  voliunlem3  25529  voliun  25531  uniioombllem2  25560  vitalilem4  25588  vitalilem5  25589  dvnfval  25899  mtestbdd  26383  radcnv0  26394  radcnvlt1  26396  radcnvle  26398  psercn  26404  pserdvlem2  26406  abelthlem1  26409  abelthlem3  26411  logtayl  26637  atantayl2  26915  atantayl3  26916  lgamgulm2  27013  lgamcvglem  27017  lgsval  27278  lgsval4  27294  lgsneg  27298  lgsmod  27300  dchrmusumlema  27470  dchrisum0lema  27491  faclim  35944  prodeq12sdv  36416  cbvsumdavw  36477  cbvproddavw  36478  cbvsumdavw2  36493  cbvproddavw2  36494  knoppcnlem9  36777  knoppndvlem4  36791  ovoliunnfl  37997  voliunnfl  37999  radcnvrat  44759  dvradcnv2  44792  binomcxplemcvg  44799  binomcxplemdvsum  44800  binomcxplemnotnn0  44801  sumnnodd  46078  stirlinglem5  46524  sge0isummpt2  46878  ovolval2lem  47089