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