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

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 )