Metamath Proof Explorer


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 𝑦