Theorem seqeq3d 13969

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

Syntax hints:   → wi 4   = wceq 1547  seqcseq 13961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-xp 5631  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6259  df-iota 6448  df-fv 6500  df-ov 7366  df-oprab 7367  df-mpo 7368  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-seq 13962

This theorem is referenced by:  seqeq123d  13970  seqf1olem2  14002  seqf1o  14003  seqof2  14020  expval  14023  relexp1g  14986  sumeq1  15649  sumeq2w  15652  cbvsum  15655  cbvsumv  15656  sumeq2sdv  15663  summo  15677  fsum  15680  geomulcvg  15839  prodeq1f  15869  prodeq1  15870  prodeq2w  15873  prodeq2sdv  15886  prodmo  15899  fprod  15904  gsumvalx  18642  mulgval  19045  gsumval3eu  19877  gsumval3lem2  19879  gsumzres  19882  gsumzf1o  19885  elovolmr  25468  ovolctb  25482  ovoliunlem3  25496  ovoliunnul  25499  ovolshftlem1  25501  voliunlem3  25544  voliun  25546  uniioombllem2  25575  vitalilem4  25603  vitalilem5  25604  dvnfval  25914  mtestbdd  26395  radcnv0  26406  radcnvlt1  26408  radcnvle  26410  psercn  26416  pserdvlem2  26418  abelthlem1  26421  abelthlem3  26423  logtayl  26649  atantayl2  26927  atantayl3  26928  lgamgulm2  27024  lgamcvglem  27028  lgsval  27289  lgsval4  27305  lgsneg  27309  lgsmod  27311  dchrmusumlema  27481  dchrisum0lema  27502  faclim  35981  prodeq12sdv  36453  cbvsumdavw  36514  cbvproddavw  36515  cbvsumdavw2  36530  cbvproddavw2  36531  knoppcnlem9  36814  knoppndvlem4  36828  ovoliunnfl  38036  voliunnfl  38038  radcnvrat  44765  dvradcnv2  44798  binomcxplemcvg  44805  binomcxplemdvsum  44806  binomcxplemnotnn0  44807  sumnnodd  46082  stirlinglem5  46528  sge0isummpt2  46882  ovolval2lem  47093