Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Gino Giotto
Equality theorems.
Inference versions.
itgeq1i
Next ⟩
itgeq2i
Metamath Proof Explorer
Ascii
Unicode
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
d
x
=
∫
B
C
d
x
Proof
Step
Hyp
Ref
Expression
1
itgeq1i.1
⊢
A
=
B
2
eqid
⊢
C
=
C
3
1
2
itgeq12i
⊢
∫
A
C
d
x
=
∫
B
C
d
x