Theorem seqeq3d 13981

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

Syntax hints:   → wi 4   = wceq 1540  seqcseq 13973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-xp 5647  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-iota 6467  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-seq 13974

This theorem is referenced by:  seqeq123d  13982  seqf1olem2  14014  seqf1o  14015  seqof2  14032  expval  14035  relexp1g  14999  sumeq1  15662  sumeq2w  15665  cbvsum  15668  cbvsumv  15669  sumeq2sdv  15676  summo  15690  fsum  15693  geomulcvg  15849  prodeq1f  15879  prodeq1  15880  prodeq2w  15883  prodeq2sdv  15896  prodmo  15909  fprod  15914  gsumvalx  18610  mulgval  19010  gsumval3eu  19841  gsumval3lem2  19843  gsumzres  19846  gsumzf1o  19849  elovolmr  25384  ovolctb  25398  ovoliunlem3  25412  ovoliunnul  25415  ovolshftlem1  25417  voliunlem3  25460  voliun  25462  uniioombllem2  25491  vitalilem4  25519  vitalilem5  25520  dvnfval  25831  mtestbdd  26321  radcnv0  26332  radcnvlt1  26334  radcnvle  26336  psercn  26343  pserdvlem2  26345  abelthlem1  26348  abelthlem3  26350  logtayl  26576  atantayl2  26855  atantayl3  26856  lgamgulm2  26953  lgamcvglem  26957  lgsval  27219  lgsval4  27235  lgsneg  27239  lgsmod  27241  dchrmusumlema  27411  dchrisum0lema  27432  faclim  35740  prodeq12sdv  36213  cbvsumdavw  36274  cbvproddavw  36275  cbvsumdavw2  36290  cbvproddavw2  36291  knoppcnlem9  36496  knoppndvlem4  36510  ovoliunnfl  37663  voliunnfl  37665  radcnvrat  44310  dvradcnv2  44343  binomcxplemcvg  44350  binomcxplemdvsum  44351  binomcxplemnotnn0  44352  sumnnodd  45635  stirlinglem5  46083  sge0isummpt2  46437  ovolval2lem  46648