Metamath Proof Explorer


Theorem itgeq1

Description: Equality theorem for an integral. (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Assertion itgeq1
|- ( A = B -> S. A C _d x = S. B C _d x )

Proof

Step Hyp Ref Expression
1 nfcv
 |-  F/_ x A
2 nfcv
 |-  F/_ x B
3 1 2 itgeq1f
 |-  ( A = B -> S. A C _d x = S. B C _d x )