Metamath Proof Explorer


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 )