Theorem cbvditgv

Description: Change bound variable in a directed integral. (Contributed by Mario Carneiro, 7-Sep-2014)

	Ref	Expression
Hypothesis	cbvditg.1	⊢ ( 𝑥 = 𝑦 → 𝐶 = 𝐷 )
Assertion	cbvditgv	⊢ ⨜ [ 𝐴 → 𝐵 ] 𝐶 d 𝑥 = ⨜ [ 𝐴 → 𝐵 ] 𝐷 d 𝑦

Proof

Step	Hyp	Ref	Expression
1		cbvditg.1	⊢ ( 𝑥 = 𝑦 → 𝐶 = 𝐷 )
2		nfcv	⊢ Ⅎ 𝑦 𝐶
3		nfcv	⊢ Ⅎ 𝑥 𝐷
4	1 2 3	cbvditg	⊢ ⨜ [ 𝐴 → 𝐵 ] 𝐶 d 𝑥 = ⨜ [ 𝐴 → 𝐵 ] 𝐷 d 𝑦