Metamath Proof Explorer


Theorem itgeq1i

Description: Equality inference for an integral. (Contributed by GG, 1-Sep-2025)

Ref Expression
Hypothesis itgeq1i.1 ⊢ A = B
Assertion itgeq1i ⊢ ∫ A C dx = ∫ B C dx

Proof

Step Hyp Ref Expression
1 itgeq1i.1 ⊢ A = B
2 eqid ⊢ C = C
3 1 2 itgeq12i ⊢ ∫ A C dx = ∫ B C dx