This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \to C = D$
	Assertion	cbvditgv	$⊢ \int_{A}^{B} C d x = \int_{A}^{B} D d y$

Step	Hyp	Ref	Expression
1		cbvditg.1	$⊢ x = y \to C = D$
2		nfcv	$⊢ \underline{Ⅎ} y C$
3		nfcv	$⊢ \underline{Ⅎ} x D$
4	1 2 3	cbvditg	$⊢ \int_{A}^{B} C d x = \int_{A}^{B} D d y$