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}Bdx={\int }_A\left(x\in A⟼B\right)\left(y\right)dy$$

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\left(x\in A⟼B\right)\left(y\right)$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}y\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)dy={\int }_A\left(x\in A⟼B\right)\left(x\right)dx$$
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)dx={\int }_{A}Bdx$$
11	5 10	syl5req	$$⊢\phi \to {\int }_{A}Bdx={\int }_A\left(x\in A⟼B\right)\left(y\right)dy$$