# Metamath Proof Explorer

## Theorem itgmpt

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

Ref Expression
Hypothesis itgmpt.1 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {V}$
Assertion itgmpt ${⊢}{\phi }\to {\int }_{{A}}{B}d{x}={\int }_{{A}}\left({x}\in {A}⟼{B}\right)\left({y}\right)d{y}$

### Proof

Step Hyp Ref Expression
1 itgmpt.1 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {V}$
2 fveq2 ${⊢}{y}={x}\to \left({x}\in {A}⟼{B}\right)\left({y}\right)=\left({x}\in {A}⟼{B}\right)\left({x}\right)$
3 nffvmpt1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}⟼{B}\right)\left({y}\right)$
4 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}⟼{B}\right)\left({x}\right)$
5 2 3 4 cbvitg ${⊢}{\int }_{{A}}\left({x}\in {A}⟼{B}\right)\left({y}\right)d{y}={\int }_{{A}}\left({x}\in {A}⟼{B}\right)\left({x}\right)d{x}$
6 simpr ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {x}\in {A}$
7 eqid ${⊢}\left({x}\in {A}⟼{B}\right)=\left({x}\in {A}⟼{B}\right)$
8 7 fvmpt2 ${⊢}\left({x}\in {A}\wedge {B}\in {V}\right)\to \left({x}\in {A}⟼{B}\right)\left({x}\right)={B}$
9 6 1 8 syl2anc ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({x}\in {A}⟼{B}\right)\left({x}\right)={B}$
10 9 itgeq2dv ${⊢}{\phi }\to {\int }_{{A}}\left({x}\in {A}⟼{B}\right)\left({x}\right)d{x}={\int }_{{A}}{B}d{x}$
11 5 10 syl5req ${⊢}{\phi }\to {\int }_{{A}}{B}d{x}={\int }_{{A}}\left({x}\in {A}⟼{B}\right)\left({y}\right)d{y}$