Theorem seqeq3d 13934

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

Syntax hints:   → wi 4   = wceq 1540  seqcseq 13926

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-xp 5629  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-iota 6442  df-fv 6494  df-ov 7356  df-oprab 7357  df-mpo 7358  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-seq 13927

This theorem is referenced by:  seqeq123d  13935  seqf1olem2  13967  seqf1o  13968  seqof2  13985  expval  13988  relexp1g  14951  sumeq1  15614  sumeq2w  15617  cbvsum  15620  cbvsumv  15621  sumeq2sdv  15628  summo  15642  fsum  15645  geomulcvg  15801  prodeq1f  15831  prodeq1  15832  prodeq2w  15835  prodeq2sdv  15848  prodmo  15861  fprod  15866  gsumvalx  18568  mulgval  18968  gsumval3eu  19801  gsumval3lem2  19803  gsumzres  19806  gsumzf1o  19809  elovolmr  25393  ovolctb  25407  ovoliunlem3  25421  ovoliunnul  25424  ovolshftlem1  25426  voliunlem3  25469  voliun  25471  uniioombllem2  25500  vitalilem4  25528  vitalilem5  25529  dvnfval  25840  mtestbdd  26330  radcnv0  26341  radcnvlt1  26343  radcnvle  26345  psercn  26352  pserdvlem2  26354  abelthlem1  26357  abelthlem3  26359  logtayl  26585  atantayl2  26864  atantayl3  26865  lgamgulm2  26962  lgamcvglem  26966  lgsval  27228  lgsval4  27244  lgsneg  27248  lgsmod  27250  dchrmusumlema  27420  dchrisum0lema  27441  faclim  35718  prodeq12sdv  36191  cbvsumdavw  36252  cbvproddavw  36253  cbvsumdavw2  36268  cbvproddavw2  36269  knoppcnlem9  36474  knoppndvlem4  36488  ovoliunnfl  37641  voliunnfl  37643  radcnvrat  44287  dvradcnv2  44320  binomcxplemcvg  44327  binomcxplemdvsum  44328  binomcxplemnotnn0  44329  sumnnodd  45612  stirlinglem5  46060  sge0isummpt2  46414  ovolval2lem  46625