Theorem seqeq3d 13926

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

Syntax hints:   → wi 4   = wceq 1541  seqcseq 13918

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3050  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-xp 5627  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-iota 6445  df-fv 6497  df-ov 7358  df-oprab 7359  df-mpo 7360  df-frecs 8220  df-wrecs 8251  df-recs 8300  df-rdg 8338  df-seq 13919

This theorem is referenced by:  seqeq123d  13927  seqf1olem2  13959  seqf1o  13960  seqof2  13977  expval  13980  relexp1g  14943  sumeq1  15606  sumeq2w  15609  cbvsum  15612  cbvsumv  15613  sumeq2sdv  15620  summo  15634  fsum  15637  geomulcvg  15793  prodeq1f  15823  prodeq1  15824  prodeq2w  15827  prodeq2sdv  15840  prodmo  15853  fprod  15858  gsumvalx  18594  mulgval  18994  gsumval3eu  19826  gsumval3lem2  19828  gsumzres  19831  gsumzf1o  19834  elovolmr  25414  ovolctb  25428  ovoliunlem3  25442  ovoliunnul  25445  ovolshftlem1  25447  voliunlem3  25490  voliun  25492  uniioombllem2  25521  vitalilem4  25549  vitalilem5  25550  dvnfval  25861  mtestbdd  26351  radcnv0  26362  radcnvlt1  26364  radcnvle  26366  psercn  26373  pserdvlem2  26375  abelthlem1  26378  abelthlem3  26380  logtayl  26606  atantayl2  26885  atantayl3  26886  lgamgulm2  26983  lgamcvglem  26987  lgsval  27249  lgsval4  27265  lgsneg  27269  lgsmod  27271  dchrmusumlema  27441  dchrisum0lema  27462  faclim  35801  prodeq12sdv  36273  cbvsumdavw  36334  cbvproddavw  36335  cbvsumdavw2  36350  cbvproddavw2  36351  knoppcnlem9  36556  knoppndvlem4  36570  ovoliunnfl  37712  voliunnfl  37714  radcnvrat  44421  dvradcnv2  44454  binomcxplemcvg  44461  binomcxplemdvsum  44462  binomcxplemnotnn0  44463  sumnnodd  45744  stirlinglem5  46190  sge0isummpt2  46544  ovolval2lem  46755