Metamath Proof Explorer


Theorem itgeq1

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

Ref Expression
Assertion itgeq1 ( 𝐴 = 𝐵 → ∫ 𝐴 𝐶 d 𝑥 = ∫ 𝐵 𝐶 d 𝑥 )

Proof

Step Hyp Ref Expression
1 nfcv 𝑥 𝐴
2 nfcv 𝑥 𝐵
3 1 2 itgeq1f ( 𝐴 = 𝐵 → ∫ 𝐴 𝐶 d 𝑥 = ∫ 𝐵 𝐶 d 𝑥 )