Theorem cbvditgvw2

Description: Change bound variable and domain in a directed integral, using implicit substitution. (Contributed by GG, 1-Sep-2025)

	Ref	Expression
Hypotheses	cbvditgvw2.1	⊢ 𝐴 = 𝐵
	cbvditgvw2.2	⊢ 𝐶 = 𝐷
	cbvditgvw2.3	⊢ ( 𝑥 = 𝑦 → 𝐸 = 𝐹 )
Assertion	cbvditgvw2	⊢ ⨜ [ 𝐴 → 𝐶 ] 𝐸 d 𝑥 = ⨜ [ 𝐵 → 𝐷 ] 𝐹 d 𝑦

Proof

Step	Hyp	Ref	Expression
1		cbvditgvw2.1	⊢ 𝐴 = 𝐵
2		cbvditgvw2.2	⊢ 𝐶 = 𝐷
3		cbvditgvw2.3	⊢ ( 𝑥 = 𝑦 → 𝐸 = 𝐹 )
4	1 2	breq12i	⊢ ( 𝐴 ≤ 𝐶 ↔ 𝐵 ≤ 𝐷 )
5	1 2	oveq12i	⊢ ( 𝐴 (,) 𝐶 ) = ( 𝐵 (,) 𝐷 )
6	5	a1i	⊢ ( 𝑥 = 𝑦 → ( 𝐴 (,) 𝐶 ) = ( 𝐵 (,) 𝐷 ) )
7	3 6	cbvitgvw2	⊢ ∫ ( 𝐴 (,) 𝐶 ) 𝐸 d 𝑥 = ∫ ( 𝐵 (,) 𝐷 ) 𝐹 d 𝑦
8	2	a1i	⊢ ( 𝑥 = 𝑦 → 𝐶 = 𝐷 )
9	1	a1i	⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
10	8 9	oveq12d	⊢ ( 𝑥 = 𝑦 → ( 𝐶 (,) 𝐴 ) = ( 𝐷 (,) 𝐵 ) )
11	3 10	cbvitgvw2	⊢ ∫ ( 𝐶 (,) 𝐴 ) 𝐸 d 𝑥 = ∫ ( 𝐷 (,) 𝐵 ) 𝐹 d 𝑦
12	11	negeqi	⊢ - ∫ ( 𝐶 (,) 𝐴 ) 𝐸 d 𝑥 = - ∫ ( 𝐷 (,) 𝐵 ) 𝐹 d 𝑦
13	4 7 12	ifbieq12i	⊢ if ( 𝐴 ≤ 𝐶 , ∫ ( 𝐴 (,) 𝐶 ) 𝐸 d 𝑥 , - ∫ ( 𝐶 (,) 𝐴 ) 𝐸 d 𝑥 ) = if ( 𝐵 ≤ 𝐷 , ∫ ( 𝐵 (,) 𝐷 ) 𝐹 d 𝑦 , - ∫ ( 𝐷 (,) 𝐵 ) 𝐹 d 𝑦 )
14		df-ditg	⊢ ⨜ [ 𝐴 → 𝐶 ] 𝐸 d 𝑥 = if ( 𝐴 ≤ 𝐶 , ∫ ( 𝐴 (,) 𝐶 ) 𝐸 d 𝑥 , - ∫ ( 𝐶 (,) 𝐴 ) 𝐸 d 𝑥 )
15		df-ditg	⊢ ⨜ [ 𝐵 → 𝐷 ] 𝐹 d 𝑦 = if ( 𝐵 ≤ 𝐷 , ∫ ( 𝐵 (,) 𝐷 ) 𝐹 d 𝑦 , - ∫ ( 𝐷 (,) 𝐵 ) 𝐹 d 𝑦 )
16	13 14 15	3eqtr4i	⊢ ⨜ [ 𝐴 → 𝐶 ] 𝐸 d 𝑥 = ⨜ [ 𝐵 → 𝐷 ] 𝐹 d 𝑦