Theorem cbvditg

Description: Change bound variable in a directed integral. (Contributed by Mario Carneiro, 7-Sep-2014)

	Ref	Expression
Hypotheses	cbvditg.1	$$⊢x=y\to C=D$$
	cbvditg.2	$$⊢\underset{\_}{Ⅎ}yC$$
	cbvditg.3	$$⊢\underset{\_}{Ⅎ}xD$$
Assertion	cbvditg	$$⊢{\int }_A^{B}Cdx={\int }_A^{B}Ddy$$

Proof

Step	Hyp	Ref	Expression
1		cbvditg.1	$$⊢x=y\to C=D$$
2		cbvditg.2	$$⊢\underset{\_}{Ⅎ}yC$$
3		cbvditg.3	$$⊢\underset{\_}{Ⅎ}xD$$
4		biid	$$⊢A\le B\leftrightarrow A\le B$$
5	1 2 3	cbvitg	$$⊢{\int }_{\left(A,B\right)}Cdx={\int }_{\left(A,B\right)}Ddy$$
6	1 2 3	cbvitg	$$⊢{\int }_{\left(B,A\right)}Cdx={\int }_{\left(B,A\right)}Ddy$$
7	6	negeqi	$$⊢-{\int }_{\left(B,A\right)}Cdx=-{\int }_{\left(B,A\right)}Ddy$$
8	4 5 7	ifbieq12i	$$⊢if\left(A\le B,{\int }_{\left(A,B\right)}Cdx,-{\int }_{\left(B,A\right)}Cdx\right)=if\left(A\le B,{\int }_{\left(A,B\right)}Ddy,-{\int }_{\left(B,A\right)}Ddy\right)$$
9		df-ditg	$$⊢{\int }_A^{B}Cdx=if\left(A\le B,{\int }_{\left(A,B\right)}Cdx,-{\int }_{\left(B,A\right)}Cdx\right)$$
10		df-ditg	$$⊢{\int }_A^{B}Ddy=if\left(A\le B,{\int }_{\left(A,B\right)}Ddy,-{\int }_{\left(B,A\right)}Ddy\right)$$
11	8 9 10	3eqtr4i	$$⊢{\int }_A^{B}Cdx={\int }_A^{B}Ddy$$