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 )