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