Theorem seqeq3d 13973

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

Syntax hints:   → wi 4   = wceq 1541  seqcseq 13965

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-xp 5682  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-iota 6495  df-fv 6551  df-ov 7411  df-oprab 7412  df-mpo 7413  df-frecs 8265  df-wrecs 8296  df-recs 8370  df-rdg 8409  df-seq 13966

This theorem is referenced by:  seqeq123d  13974  seqf1olem2  14007  seqf1o  14008  seqof2  14025  expval  14028  relexp1g  14972  sumeq1  15634  sumeq2w  15637  cbvsum  15640  summo  15662  fsum  15665  geomulcvg  15821  prodeq1f  15851  prodeq2w  15855  prodmo  15879  fprod  15884  gsumvalx  18594  mulgval  18953  gsumval3eu  19771  gsumval3lem2  19773  gsumzres  19776  gsumzf1o  19779  elovolmr  24992  ovolctb  25006  ovoliunlem3  25020  ovoliunnul  25023  ovolshftlem1  25025  voliunlem3  25068  voliun  25070  uniioombllem2  25099  vitalilem4  25127  vitalilem5  25128  dvnfval  25438  mtestbdd  25916  radcnv0  25927  radcnvlt1  25929  radcnvle  25931  psercn  25937  pserdvlem2  25939  abelthlem1  25942  abelthlem3  25944  logtayl  26167  atantayl2  26440  atantayl3  26441  lgamgulm2  26537  lgamcvglem  26541  lgsval  26801  lgsval4  26817  lgsneg  26821  lgsmod  26823  dchrmusumlema  26993  dchrisum0lema  27014  faclim  34711  knoppcnlem9  35372  knoppndvlem4  35386  ovoliunnfl  36525  voliunnfl  36527  radcnvrat  43063  dvradcnv2  43096  binomcxplemcvg  43103  binomcxplemdvsum  43104  binomcxplemnotnn0  43105  sumnnodd  44336  stirlinglem5  44784  sge0isummpt2  45138  ovolval2lem  45349