Theorem cbvditgdavw

Description: Change bound variable in a directed integral. Deduction form. (Contributed by GG, 14-Aug-2025)

	Ref	Expression
Hypothesis	cbvditgdavw.1	$$⊢\left(\phi \wedge x=y\right)\to C=D$$
Assertion	cbvditgdavw	$$⊢\phi \to {\int }_A^{B}Cdx={\int }_A^{B}Ddy$$

Proof

Step	Hyp	Ref	Expression
1		cbvditgdavw.1	$$⊢\left(\phi \wedge x=y\right)\to C=D$$
2	1	cbvitgdavw	$$⊢\phi \to {\int }_{\left(A,B\right)}Cdx={\int }_{\left(A,B\right)}Ddy$$
3	1	cbvitgdavw	$$⊢\phi \to {\int }_{\left(B,A\right)}Cdx={\int }_{\left(B,A\right)}Ddy$$
4	3	negeqd	$$⊢\phi \to -{\int }_{\left(B,A\right)}Cdx=-{\int }_{\left(B,A\right)}Ddy$$
5	2 4	ifeq12d	$$⊢\phi \to 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)$$
6		df-ditg	$$⊢{\int }_A^{B}Cdx=if\left(A\le B,{\int }_{\left(A,B\right)}Cdx,-{\int }_{\left(B,A\right)}Cdx\right)$$
7		df-ditg	$$⊢{\int }_A^{B}Ddy=if\left(A\le B,{\int }_{\left(A,B\right)}Ddy,-{\int }_{\left(B,A\right)}Ddy\right)$$
8	5 6 7	3eqtr4g	$$⊢\phi \to {\int }_A^{B}Cdx={\int }_A^{B}Ddy$$