Theorem cbvditgdavw2

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

	Ref	Expression
Hypotheses	cbvditgdavw2.1	$$⊢\phi \to A=B$$
	cbvditgdavw2.2	$$⊢\phi \to C=D$$
	cbvditgdavw2.3	$$⊢\left(\phi \wedge x=y\right)\to E=F$$
Assertion	cbvditgdavw2	$$⊢\phi \to {\int }_A^{C}Edx={\int }_B^{D}Fdy$$

Proof

Step	Hyp	Ref	Expression
1		cbvditgdavw2.1	$$⊢\phi \to A=B$$
2		cbvditgdavw2.2	$$⊢\phi \to C=D$$
3		cbvditgdavw2.3	$$⊢\left(\phi \wedge x=y\right)\to E=F$$
4	1 2	breq12d	$$⊢\phi \to \left(A\le C\leftrightarrow B\le D\right)$$
5	1	adantr	$$⊢\left(\phi \wedge x=y\right)\to A=B$$
6	2	adantr	$$⊢\left(\phi \wedge x=y\right)\to C=D$$
7	5 6	oveq12d	$$⊢\left(\phi \wedge x=y\right)\to \left(A,C\right)=\left(B,D\right)$$
8	3 7	cbvitgdavw2	$$⊢\phi \to {\int }_{\left(A,C\right)}Edx={\int }_{\left(B,D\right)}Fdy$$
9	6 5	oveq12d	$$⊢\left(\phi \wedge x=y\right)\to \left(C,A\right)=\left(D,B\right)$$
10	3 9	cbvitgdavw2	$$⊢\phi \to {\int }_{\left(C,A\right)}Edx={\int }_{\left(D,B\right)}Fdy$$
11	10	negeqd	$$⊢\phi \to -{\int }_{\left(C,A\right)}Edx=-{\int }_{\left(D,B\right)}Fdy$$
12	4 8 11	ifbieq12d	$$⊢\phi \to if\left(A\le C,{\int }_{\left(A,C\right)}Edx,-{\int }_{\left(C,A\right)}Edx\right)=if\left(B\le D,{\int }_{\left(B,D\right)}Fdy,-{\int }_{\left(D,B\right)}Fdy\right)$$
13		df-ditg	$$⊢{\int }_A^{C}Edx=if\left(A\le C,{\int }_{\left(A,C\right)}Edx,-{\int }_{\left(C,A\right)}Edx\right)$$
14		df-ditg	$$⊢{\int }_B^{D}Fdy=if\left(B\le D,{\int }_{\left(B,D\right)}Fdy,-{\int }_{\left(D,B\right)}Fdy\right)$$
15	12 13 14	3eqtr4g	$$⊢\phi \to {\int }_A^{C}Edx={\int }_B^{D}Fdy$$