Theorem itgmpt

Description: Change bound variable in an integral. (Contributed by Mario Carneiro, 29-Jun-2014)

	Ref	Expression
Hypothesis	itgmpt.1	|- ( ( ph /\ x e. A ) -> B e. V )
Assertion	itgmpt	|- ( ph -> S. A B _d x = S. A ( ( x e. A |-> B ) ` y ) _d y )

Proof

Step	Hyp	Ref	Expression
1		itgmpt.1	|- ( ( ph /\ x e. A ) -> B e. V )
2		fveq2	|- ( y = x -> ( ( x e. A |-> B ) ` y ) = ( ( x e. A |-> B ) ` x ) )
3		nffvmpt1	|- F/_ x ( ( x e. A |-> B ) ` y )
4		nfcv	|- F/_ y ( ( x e. A |-> B ) ` x )
5	2 3 4	cbvitg	|- S. A ( ( x e. A |-> B ) ` y ) _d y = S. A ( ( x e. A |-> B ) ` x ) _d x
6		simpr	|- ( ( ph /\ x e. A ) -> x e. A )
7		eqid	|- ( x e. A |-> B ) = ( x e. A |-> B )
8	7	fvmpt2	|- ( ( x e. A /\ B e. V ) -> ( ( x e. A |-> B ) ` x ) = B )
9	6 1 8	syl2anc	|- ( ( ph /\ x e. A ) -> ( ( x e. A |-> B ) ` x ) = B )
10	9	itgeq2dv	|- ( ph -> S. A ( ( x e. A |-> B ) ` x ) _d x = S. A B _d x )
11	5 10	eqtr2id	|- ( ph -> S. A B _d x = S. A ( ( x e. A |-> B ) ` y ) _d y )