Metamath Proof Explorer


Theorem itgmpt

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

Ref Expression
Hypothesis itgmpt.1 φ x A B V
Assertion itgmpt φ A B dx = A x A B y dy

Proof

Step Hyp Ref Expression
1 itgmpt.1 φ x A B V
2 fveq2 y = x x A B y = x A B x
3 nffvmpt1 _ x x A B y
4 nfcv _ y x A B x
5 2 3 4 cbvitg A x A B y dy = A x A B x dx
6 simpr φ x A x A
7 eqid x A B = x A B
8 7 fvmpt2 x A B V x A B x = B
9 6 1 8 syl2anc φ x A x A B x = B
10 9 itgeq2dv φ A x A B x dx = A B dx
11 5 10 eqtr2id φ A B dx = A x A B y dy