Theorem itgmpt

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

	Ref	Expression
Hypothesis	itgmpt.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
Assertion	itgmpt	⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 = ∫ 𝐴 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) d 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		itgmpt.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
2		fveq2	⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
3		nffvmpt1	⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 )
4		nfcv	⊢ Ⅎ 𝑦 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 )
5	2 3 4	cbvitg	⊢ ∫ 𝐴 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) d 𝑦 = ∫ 𝐴 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) d 𝑥
6		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
7		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
8	7	fvmpt2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
9	6 1 8	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
10	9	itgeq2dv	⊢ ( 𝜑 → ∫ 𝐴 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) d 𝑥 = ∫ 𝐴 𝐵 d 𝑥 )
11	5 10	syl5req	⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 = ∫ 𝐴 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) d 𝑦 )