Theorem seqeq3d 14047

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

Syntax hints:   → wi 4   = wceq 1537  seqcseq 14039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-xp 5695  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-iota 6516  df-fv 6571  df-ov 7434  df-oprab 7435  df-mpo 7436  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-seq 14040

This theorem is referenced by:  seqeq123d  14048  seqf1olem2  14080  seqf1o  14081  seqof2  14098  expval  14101  relexp1g  15062  sumeq1  15722  sumeq2w  15725  cbvsum  15728  cbvsumv  15729  sumeq2sdv  15736  summo  15750  fsum  15753  geomulcvg  15909  prodeq1f  15939  prodeq1  15940  prodeq2w  15943  prodeq2sdv  15956  prodmo  15969  fprod  15974  gsumvalx  18702  mulgval  19102  gsumval3eu  19937  gsumval3lem2  19939  gsumzres  19942  gsumzf1o  19945  elovolmr  25525  ovolctb  25539  ovoliunlem3  25553  ovoliunnul  25556  ovolshftlem1  25558  voliunlem3  25601  voliun  25603  uniioombllem2  25632  vitalilem4  25660  vitalilem5  25661  dvnfval  25973  mtestbdd  26463  radcnv0  26474  radcnvlt1  26476  radcnvle  26478  psercn  26485  pserdvlem2  26487  abelthlem1  26490  abelthlem3  26492  logtayl  26717  atantayl2  26996  atantayl3  26997  lgamgulm2  27094  lgamcvglem  27098  lgsval  27360  lgsval4  27376  lgsneg  27380  lgsmod  27382  dchrmusumlema  27552  dchrisum0lema  27573  faclim  35726  prodeq12sdv  36201  cbvsumdavw  36262  cbvproddavw  36263  cbvsumdavw2  36278  cbvproddavw2  36279  knoppcnlem9  36484  knoppndvlem4  36498  ovoliunnfl  37649  voliunnfl  37651  radcnvrat  44310  dvradcnv2  44343  binomcxplemcvg  44350  binomcxplemdvsum  44351  binomcxplemnotnn0  44352  sumnnodd  45586  stirlinglem5  46034  sge0isummpt2  46388  ovolval2lem  46599