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 1540  seqcseq 13966

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-xp 5644  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-iota 6464  df-fv 6519  df-ov 7390  df-oprab 7391  df-mpo 7392  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-seq 13967

This theorem is referenced by:  seqeq123d  13975  seqf1olem2  14007  seqf1o  14008  seqof2  14025  expval  14028  relexp1g  14992  sumeq1  15655  sumeq2w  15658  cbvsum  15661  cbvsumv  15662  sumeq2sdv  15669  summo  15683  fsum  15686  geomulcvg  15842  prodeq1f  15872  prodeq1  15873  prodeq2w  15876  prodeq2sdv  15889  prodmo  15902  fprod  15907  gsumvalx  18603  mulgval  19003  gsumval3eu  19834  gsumval3lem2  19836  gsumzres  19839  gsumzf1o  19842  elovolmr  25377  ovolctb  25391  ovoliunlem3  25405  ovoliunnul  25408  ovolshftlem1  25410  voliunlem3  25453  voliun  25455  uniioombllem2  25484  vitalilem4  25512  vitalilem5  25513  dvnfval  25824  mtestbdd  26314  radcnv0  26325  radcnvlt1  26327  radcnvle  26329  psercn  26336  pserdvlem2  26338  abelthlem1  26341  abelthlem3  26343  logtayl  26569  atantayl2  26848  atantayl3  26849  lgamgulm2  26946  lgamcvglem  26950  lgsval  27212  lgsval4  27228  lgsneg  27232  lgsmod  27234  dchrmusumlema  27404  dchrisum0lema  27425  faclim  35733  prodeq12sdv  36206  cbvsumdavw  36267  cbvproddavw  36268  cbvsumdavw2  36283  cbvproddavw2  36284  knoppcnlem9  36489  knoppndvlem4  36503  ovoliunnfl  37656  voliunnfl  37658  radcnvrat  44303  dvradcnv2  44336  binomcxplemcvg  44343  binomcxplemdvsum  44344  binomcxplemnotnn0  44345  sumnnodd  45628  stirlinglem5  46076  sge0isummpt2  46430  ovolval2lem  46641