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	⊢ ( 𝜑 → 𝐴 = 𝐵 )
	cbvditgdavw2.2	⊢ ( 𝜑 → 𝐶 = 𝐷 )
	cbvditgdavw2.3	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → 𝐸 = 𝐹 )
Assertion	cbvditgdavw2	⊢ ( 𝜑 → ⨜ [ 𝐴 → 𝐶 ] 𝐸 d 𝑥 = ⨜ [ 𝐵 → 𝐷 ] 𝐹 d 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		cbvditgdavw2.1	⊢ ( 𝜑 → 𝐴 = 𝐵 )
2		cbvditgdavw2.2	⊢ ( 𝜑 → 𝐶 = 𝐷 )
3		cbvditgdavw2.3	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → 𝐸 = 𝐹 )
4	1 2	breq12d	⊢ ( 𝜑 → ( 𝐴 ≤ 𝐶 ↔ 𝐵 ≤ 𝐷 ) )
5	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → 𝐴 = 𝐵 )
6	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → 𝐶 = 𝐷 )
7	5 6	oveq12d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → ( 𝐴 (,) 𝐶 ) = ( 𝐵 (,) 𝐷 ) )
8	3 7	cbvitgdavw2	⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐶 ) 𝐸 d 𝑥 = ∫ ( 𝐵 (,) 𝐷 ) 𝐹 d 𝑦 )
9	6 5	oveq12d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → ( 𝐶 (,) 𝐴 ) = ( 𝐷 (,) 𝐵 ) )
10	3 9	cbvitgdavw2	⊢ ( 𝜑 → ∫ ( 𝐶 (,) 𝐴 ) 𝐸 d 𝑥 = ∫ ( 𝐷 (,) 𝐵 ) 𝐹 d 𝑦 )
11	10	negeqd	⊢ ( 𝜑 → - ∫ ( 𝐶 (,) 𝐴 ) 𝐸 d 𝑥 = - ∫ ( 𝐷 (,) 𝐵 ) 𝐹 d 𝑦 )
12	4 8 11	ifbieq12d	⊢ ( 𝜑 → if ( 𝐴 ≤ 𝐶 , ∫ ( 𝐴 (,) 𝐶 ) 𝐸 d 𝑥 , - ∫ ( 𝐶 (,) 𝐴 ) 𝐸 d 𝑥 ) = if ( 𝐵 ≤ 𝐷 , ∫ ( 𝐵 (,) 𝐷 ) 𝐹 d 𝑦 , - ∫ ( 𝐷 (,) 𝐵 ) 𝐹 d 𝑦 ) )
13		df-ditg	⊢ ⨜ [ 𝐴 → 𝐶 ] 𝐸 d 𝑥 = if ( 𝐴 ≤ 𝐶 , ∫ ( 𝐴 (,) 𝐶 ) 𝐸 d 𝑥 , - ∫ ( 𝐶 (,) 𝐴 ) 𝐸 d 𝑥 )
14		df-ditg	⊢ ⨜ [ 𝐵 → 𝐷 ] 𝐹 d 𝑦 = if ( 𝐵 ≤ 𝐷 , ∫ ( 𝐵 (,) 𝐷 ) 𝐹 d 𝑦 , - ∫ ( 𝐷 (,) 𝐵 ) 𝐹 d 𝑦 )
15	12 13 14	3eqtr4g	⊢ ( 𝜑 → ⨜ [ 𝐴 → 𝐶 ] 𝐸 d 𝑥 = ⨜ [ 𝐵 → 𝐷 ] 𝐹 d 𝑦 )