Theorem seqeq3d 13974

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

Syntax hints:   → wi 4   = wceq 1542  seqcseq 13966

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-xp 5683  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-iota 6496  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-seq 13967

This theorem is referenced by:  seqeq123d  13975  seqf1olem2  14008  seqf1o  14009  seqof2  14026  expval  14029  relexp1g  14973  sumeq1  15635  sumeq2w  15638  cbvsum  15641  summo  15663  fsum  15666  geomulcvg  15822  prodeq1f  15852  prodeq2w  15856  prodmo  15880  fprod  15885  gsumvalx  18595  mulgval  18954  gsumval3eu  19772  gsumval3lem2  19774  gsumzres  19777  gsumzf1o  19780  elovolmr  24993  ovolctb  25007  ovoliunlem3  25021  ovoliunnul  25024  ovolshftlem1  25026  voliunlem3  25069  voliun  25071  uniioombllem2  25100  vitalilem4  25128  vitalilem5  25129  dvnfval  25439  mtestbdd  25917  radcnv0  25928  radcnvlt1  25930  radcnvle  25932  psercn  25938  pserdvlem2  25940  abelthlem1  25943  abelthlem3  25945  logtayl  26168  atantayl2  26443  atantayl3  26444  lgamgulm2  26540  lgamcvglem  26544  lgsval  26804  lgsval4  26820  lgsneg  26824  lgsmod  26826  dchrmusumlema  26996  dchrisum0lema  27017  faclim  34716  knoppcnlem9  35377  knoppndvlem4  35391  ovoliunnfl  36530  voliunnfl  36532  radcnvrat  43073  dvradcnv2  43106  binomcxplemcvg  43113  binomcxplemdvsum  43114  binomcxplemnotnn0  43115  sumnnodd  44346  stirlinglem5  44794  sge0isummpt2  45148  ovolval2lem  45359