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 18	1 ⊢ (𝜑 → seq𝑀( + , 𝐴) = seq𝑀( + , 𝐵))

Syntax hints:   → wi 4   = wceq 1570  seqcseq 14039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-xp 5669  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6304  df-iota 6494  df-fv 6546  df-ov 7415  df-oprab 7416  df-mpo 7417  df-frecs 8279  df-wrecs 8310  df-recs 8359  df-rdg 8398  df-seq 14040

This theorem is referenced by:  seqeq123d  14048  seqf1olem2  14080  seqf1o  14081  seqof2  14098  expval  14101  relexp1g  15065  sumeq1  15742  sumeq2w  15745  cbvsum  15748  cbvsumv  15749  sumeq2sdv  15756  summo  15770  fsum  15773  geomulcvg  15932  prodeq1f  15962  prodeq1  15963  prodeq2w  15966  prodeq2sdv  15979  prodmo  15992  fprod  15997  gsumvalx  18735  mulgval  19138  gsumval3eu  19975  gsumval3lem2  19977  gsumzres  19980  gsumzf1o  19983  elovolmr  25616  ovolctb  25630  ovoliunlem3  25644  ovoliunnul  25647  ovolshftlem1  25649  voliunlem3  25692  voliun  25694  uniioombllem2  25723  vitalilem4  25751  vitalilem5  25752  dvnfval  26062  mtestbdd  26546  radcnv0  26557  radcnvlt1  26559  radcnvle  26561  psercn  26567  pserdvlem2  26569  abelthlem1  26572  abelthlem3  26574  logtayl  26803  atantayl2  27081  atantayl3  27082  lgamgulm2  27178  lgamcvglem  27182  lgsval  27443  lgsval4  27459  lgsneg  27463  lgsmod  27465  dchrmusumlema  27635  dchrisum0lema  27656  faclim  36216  prodeq12sdv  36708  cbvsumdavw  36769  cbvproddavw  36770  cbvsumdavw2  36785  cbvproddavw2  36786  knoppcnlem9  37068  knoppndvlem4  37082  ovoliunnfl  38291  voliunnfl  38293  radcnvrat  45004  dvradcnv2  45037  binomcxplemcvg  45044  binomcxplemdvsum  45045  binomcxplemnotnn0  45046  sumnnodd  46326  stirlinglem5  46772  sge0isummpt2  47126  ovolval2lem  47337