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 
|- S. A C _d x = S. B C _d x

Proof

Step Hyp Ref Expression
1 itgeq1i.1 
 |-  A = B
2 eqid 
 |-  C = C
3 1 2 itgeq12i 
 |-  S. A C _d x = S. B C _d x