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
|- ( x = y -> C = D )
Assertion cbvditgv
|- S_ [ A -> B ] C _d x = S_ [ A -> B ] D _d y

Proof

Step Hyp Ref Expression
1 cbvditg.1
 |-  ( x = y -> C = D )
2 nfcv
 |-  F/_ y C
3 nfcv
 |-  F/_ x D
4 1 2 3 cbvditg
 |-  S_ [ A -> B ] C _d x = S_ [ A -> B ] D _d y