Theorem itgeq2dv

Description: Equality theorem for an integral. (Contributed by Mario Carneiro, 7-Jul-2014)

	Ref	Expression
Hypothesis	itgeq2dv.1	|- ( ( ph /\ x e. A ) -> B = C )
Assertion	itgeq2dv	|- ( ph -> S. A B _d x = S. A C _d x )

Proof

Step	Hyp	Ref	Expression
1		itgeq2dv.1	|- ( ( ph /\ x e. A ) -> B = C )
2	1	ralrimiva	|- ( ph -> A. x e. A B = C )
3		itgeq2	|- ( A. x e. A B = C -> S. A B _d x = S. A C _d x )
4	2 3	syl	|- ( ph -> S. A B _d x = S. A C _d x )