Theorem seqeq3d 13944

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

Syntax hints:   → wi 4   = wceq 1542  seqcseq 13936

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-xp 5638  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-iota 6456  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-seq 13937

This theorem is referenced by:  seqeq123d  13945  seqf1olem2  13977  seqf1o  13978  seqof2  13995  expval  13998  relexp1g  14961  sumeq1  15624  sumeq2w  15627  cbvsum  15630  cbvsumv  15631  sumeq2sdv  15638  summo  15652  fsum  15655  geomulcvg  15811  prodeq1f  15841  prodeq1  15842  prodeq2w  15845  prodeq2sdv  15858  prodmo  15871  fprod  15876  gsumvalx  18613  mulgval  19013  gsumval3eu  19845  gsumval3lem2  19847  gsumzres  19850  gsumzf1o  19853  elovolmr  25445  ovolctb  25459  ovoliunlem3  25473  ovoliunnul  25476  ovolshftlem1  25478  voliunlem3  25521  voliun  25523  uniioombllem2  25552  vitalilem4  25580  vitalilem5  25581  dvnfval  25892  mtestbdd  26382  radcnv0  26393  radcnvlt1  26395  radcnvle  26397  psercn  26404  pserdvlem2  26406  abelthlem1  26409  abelthlem3  26411  logtayl  26637  atantayl2  26916  atantayl3  26917  lgamgulm2  27014  lgamcvglem  27018  lgsval  27280  lgsval4  27296  lgsneg  27300  lgsmod  27302  dchrmusumlema  27472  dchrisum0lema  27493  faclim  35959  prodeq12sdv  36431  cbvsumdavw  36492  cbvproddavw  36493  cbvsumdavw2  36508  cbvproddavw2  36509  knoppcnlem9  36720  knoppndvlem4  36734  ovoliunnfl  37907  voliunnfl  37909  radcnvrat  44664  dvradcnv2  44697  binomcxplemcvg  44704  binomcxplemdvsum  44705  binomcxplemnotnn0  44706  sumnnodd  45984  stirlinglem5  46430  sge0isummpt2  46784  ovolval2lem  46995