Theorem seqeq3d 14065

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  seqcseq 14057

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-xp 5672  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6309  df-iota 6499  df-fv 6551  df-ov 7426  df-oprab 7427  df-mpo 7428  df-frecs 8287  df-wrecs 8318  df-recs 8367  df-rdg 8406  df-seq 14058

This theorem is used by:  seqeq123d  14066  seqf1olem2  14098  seqf1o  14099  seqof2  14116  expval  14119  relexp1g  15089  sumeq1  15766  sumeq2w  15769  cbvsum  15772  cbvsumv  15773  sumeq2sdv  15780  summo  15794  fsum  15797  geomulcvg  15956  prodeq1f  15986  prodeq1  15987  prodeq2w  15990  prodeq2sdv  16003  prodmo  16016  fprod  16021  gsumvalx  18763  mulgval  19168  gsumval3eu  20005  gsumval3lem2  20007  gsumzres  20010  gsumzf1o  20013  elovolmr  25672  ovolctb  25686  ovoliunlem3  25700  ovoliunnul  25703  ovolshftlem1  25705  voliunlem3  25748  voliun  25750  uniioombllem2  25779  vitalilem4  25807  vitalilem5  25808  dvnfval  26118  mtestbdd  26605  radcnv0  26616  radcnvlt1  26618  radcnvle  26620  psercn  26626  pserdvlem2  26628  abelthlem1  26631  abelthlem3  26633  logtayl  26862  atantayl2  27140  atantayl3  27141  lgamgulm2  27237  lgamcvglem  27241  lgsval  27502  lgsval4  27518  lgsneg  27522  lgsmod  27524  dchrmusumlema  27694  dchrisum0lema  27715  faclim  36259  prodeq12sdv  36771  cbvsumdavw  36832  cbvproddavw  36833  cbvsumdavw2  36848  cbvproddavw2  36849  knoppcnlem9  37131  knoppndvlem4  37145  ovoliunnfl  38354  voliunnfl  38356  radcnvrat  45065  dvradcnv2  45098  binomcxplemcvg  45105  binomcxplemdvsum  45106  binomcxplemnotnn0  45107  sumnnodd  46387  stirlinglem5  46833  sge0isummpt2  47187  ovolval2lem  47398