Theorem cbvditgdavw

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

	Ref	Expression
Hypothesis	cbvditgdavw.1	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → 𝐶 = 𝐷 )
Assertion	cbvditgdavw	⊢ ( 𝜑 → ⨜ [ 𝐴 → 𝐵 ] 𝐶 d 𝑥 = ⨜ [ 𝐴 → 𝐵 ] 𝐷 d 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		cbvditgdavw.1	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → 𝐶 = 𝐷 )
2	1	cbvitgdavw	⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 = ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑦 )
3	1	cbvitgdavw	⊢ ( 𝜑 → ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥 = ∫ ( 𝐵 (,) 𝐴 ) 𝐷 d 𝑦 )
4	3	negeqd	⊢ ( 𝜑 → - ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥 = - ∫ ( 𝐵 (,) 𝐴 ) 𝐷 d 𝑦 )
5	2 4	ifeq12d	⊢ ( 𝜑 → if ( 𝐴 ≤ 𝐵 , ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 , - ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥 ) = if ( 𝐴 ≤ 𝐵 , ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑦 , - ∫ ( 𝐵 (,) 𝐴 ) 𝐷 d 𝑦 ) )
6		df-ditg	⊢ ⨜ [ 𝐴 → 𝐵 ] 𝐶 d 𝑥 = if ( 𝐴 ≤ 𝐵 , ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 , - ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥 )
7		df-ditg	⊢ ⨜ [ 𝐴 → 𝐵 ] 𝐷 d 𝑦 = if ( 𝐴 ≤ 𝐵 , ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑦 , - ∫ ( 𝐵 (,) 𝐴 ) 𝐷 d 𝑦 )
8	5 6 7	3eqtr4g	⊢ ( 𝜑 → ⨜ [ 𝐴 → 𝐵 ] 𝐶 d 𝑥 = ⨜ [ 𝐴 → 𝐵 ] 𝐷 d 𝑦 )