Theorem seqeq3d 13372

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

Syntax hints:   → wi 4   = wceq 1538  seqcseq 13364

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-xp 5525  df-cnv 5527  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-iota 6283  df-fv 6332  df-ov 7138  df-oprab 7139  df-mpo 7140  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-seq 13365

This theorem is referenced by:  seqeq123d  13373  seqf1olem2  13406  seqf1o  13407  seqof2  13424  expval  13427  relexp1g  14377  sumeq1  15037  sumeq2w  15041  cbvsum  15044  summo  15066  fsum  15069  geomulcvg  15224  prodeq1f  15254  prodeq2w  15258  prodmo  15282  fprod  15287  gsumvalx  17878  mulgval  18220  gsumval3eu  19017  gsumval3lem2  19019  gsumzres  19022  gsumzf1o  19025  elovolmr  24080  ovolctb  24094  ovoliunlem3  24108  ovoliunnul  24111  ovolshftlem1  24113  voliunlem3  24156  voliun  24158  uniioombllem2  24187  vitalilem4  24215  vitalilem5  24216  dvnfval  24525  mtestbdd  25000  radcnv0  25011  radcnvlt1  25013  radcnvle  25015  psercn  25021  pserdvlem2  25023  abelthlem1  25026  abelthlem3  25028  logtayl  25251  atantayl2  25524  atantayl3  25525  lgamgulm2  25621  lgamcvglem  25625  lgsval  25885  lgsval4  25901  lgsneg  25905  lgsmod  25907  dchrmusumlema  26077  dchrisum0lema  26098  faclim  33091  knoppcnlem9  33953  knoppndvlem4  33967  ovoliunnfl  35099  voliunnfl  35101  radcnvrat  41018  dvradcnv2  41051  binomcxplemcvg  41058  binomcxplemdvsum  41059  binomcxplemnotnn0  41060  sumnnodd  42272  stirlinglem5  42720  sge0isummpt2  43071  ovolval2lem  43282