Theorem seqeq3d 13468

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

Syntax hints:   → wi 4   = wceq 1542  seqcseq 13460

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 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-12 2179  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-ex 1787  df-nf 1791  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-ral 3058  df-rab 3062  df-v 3400  df-un 3848  df-in 3850  df-ss 3860  df-if 4415  df-sn 4517  df-pr 4519  df-op 4523  df-uni 4797  df-br 5031  df-opab 5093  df-mpt 5111  df-xp 5531  df-cnv 5533  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6129  df-iota 6297  df-fv 6347  df-ov 7173  df-oprab 7174  df-mpo 7175  df-wrecs 7976  df-recs 8037  df-rdg 8075  df-seq 13461

This theorem is referenced by:  seqeq123d  13469  seqf1olem2  13502  seqf1o  13503  seqof2  13520  expval  13523  relexp1g  14475  sumeq1  15138  sumeq2w  15142  cbvsum  15145  summo  15167  fsum  15170  geomulcvg  15324  prodeq1f  15354  prodeq2w  15358  prodmo  15382  fprod  15387  gsumvalx  18002  mulgval  18346  gsumval3eu  19143  gsumval3lem2  19145  gsumzres  19148  gsumzf1o  19151  elovolmr  24228  ovolctb  24242  ovoliunlem3  24256  ovoliunnul  24259  ovolshftlem1  24261  voliunlem3  24304  voliun  24306  uniioombllem2  24335  vitalilem4  24363  vitalilem5  24364  dvnfval  24674  mtestbdd  25152  radcnv0  25163  radcnvlt1  25165  radcnvle  25167  psercn  25173  pserdvlem2  25175  abelthlem1  25178  abelthlem3  25180  logtayl  25403  atantayl2  25676  atantayl3  25677  lgamgulm2  25773  lgamcvglem  25777  lgsval  26037  lgsval4  26053  lgsneg  26057  lgsmod  26059  dchrmusumlema  26229  dchrisum0lema  26250  faclim  33285  knoppcnlem9  34324  knoppndvlem4  34338  ovoliunnfl  35462  voliunnfl  35464  radcnvrat  41490  dvradcnv2  41523  binomcxplemcvg  41530  binomcxplemdvsum  41531  binomcxplemnotnn0  41532  sumnnodd  42733  stirlinglem5  43181  sge0isummpt2  43532  ovolval2lem  43743