Theorem seqeq3d 14076

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

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

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 2147  ax-9 2155  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-xp 5661  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-iota 6489  df-fv 6541  df-ov 7417  df-oprab 7418  df-mpo 7419  df-frecs 8281  df-wrecs 8312  df-recs 8361  df-rdg 8400  df-seq 14069

This theorem is used by:  seqeq123d  14077  seqf1olem2  14109  seqf1o  14110  seqof2  14127  expval  14130  relexp1g  15102  sumeq1  15779  sumeq2w  15782  cbvsum  15785  cbvsumv  15786  sumeq2sdv  15793  summo  15806  fsum  15809  geomulcvg  15968  prodeq1f  15998  prodeq1  15999  prodeq2w  16002  prodeq2sdv  16014  prodmo  16026  fprod  16031  gsumvalx  18781  mulgval  19197  gsumval3eu  20034  gsumval3lem2  20036  gsumzres  20039  gsumzf1o  20042  elovolmr  25707  ovolctb  25721  ovoliunlem3  25735  ovoliunnul  25738  ovolshftlem1  25740  voliunlem3  25783  voliun  25785  uniioombllem2  25814  vitalilem4  25842  vitalilem5  25843  dvnfval  26152  mtestbdd  26644  radcnv0  26655  radcnvlt1  26657  radcnvle  26659  psercn  26665  pserdvlem2  26667  abelthlem1  26670  abelthlem3  26672  logtayl  26900  atantayl2  27178  atantayl3  27179  lgamgulm2  27275  lgamcvglem  27279  lgsval  27540  lgsval4  27556  lgsneg  27560  lgsmod  27562  dchrmusumlema  27732  dchrisum0lema  27753  faclim  36328  prodeq12sdv  36841  cbvsumdavw  36902  cbvproddavw  36903  cbvsumdavw2  36918  cbvproddavw2  36919  knoppcnlem9  37201  knoppndvlem4  37215  ovoliunnfl  38414  voliunnfl  38416  radcnvrat  45141  dvradcnv2  45174  binomcxplemcvg  45181  binomcxplemdvsum  45182  binomcxplemnotnn0  45183  sumnnodd  46463  stirlinglem5  46909  sge0isummpt2  47263  ovolval2lem  47474