Description: Equality theorem for an integral. (Contributed by Mario Carneiro, 28-Jun-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | itgeq1 | ⊢ ( 𝐴 = 𝐵 → ∫ 𝐴 𝐶 d 𝑥 = ∫ 𝐵 𝐶 d 𝑥 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv | ⊢ Ⅎ 𝑥 𝐴 | |
2 | nfcv | ⊢ Ⅎ 𝑥 𝐵 | |
3 | 1 2 | itgeq1f | ⊢ ( 𝐴 = 𝐵 → ∫ 𝐴 𝐶 d 𝑥 = ∫ 𝐵 𝐶 d 𝑥 ) |