This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem itgeq1d

Description: Equality theorem for an integral. (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Hypothesis	itgeq1d.aeqb	$⊢ φ \to A = B$
	Assertion	itgeq1d	$⊢ φ \to \int_{A} C d x = \int_{B} C d x$

Step	Hyp	Ref	Expression
1		itgeq1d.aeqb	$⊢ φ \to A = B$
2		itgeq1	$⊢ A = B \to \int_{A} C d x = \int_{B} C d x$
3	1 2	syl	$⊢ φ \to \int_{A} C d x = \int_{B} C d x$