Metamath Proof Explorer

Theorem cbvitgv

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

Ref Expression
Hypothesis cbvitg.1 
|- ( x = y -> B = C )
Assertion cbvitgv 
|- S. A B _d x = S. A C _d y

Proof

Step Hyp Ref Expression
1 cbvitg.1 
 |-  ( x = y -> B = C )
2 nfcv 
 |-  F/_ y B
3 nfcv 
 |-  F/_ x C
4 1 2 3 cbvitg 
 |-  S. A B _d x = S. A C _d y