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