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 ) |
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 ) |