Theorem cbvditgdavw

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

	Ref	Expression
Hypothesis	cbvditgdavw.1	|- ( ( ph /\ x = y ) -> C = D )
Assertion	cbvditgdavw	|- ( ph -> S_ [ A -> B ] C _d x = S_ [ A -> B ] D _d y )

Proof

Step	Hyp	Ref	Expression
1		cbvditgdavw.1	|- ( ( ph /\ x = y ) -> C = D )
2	1	cbvitgdavw	|- ( ph -> S. ( A (,) B ) C _d x = S. ( A (,) B ) D _d y )
3	1	cbvitgdavw	|- ( ph -> S. ( B (,) A ) C _d x = S. ( B (,) A ) D _d y )
4	3	negeqd	|- ( ph -> -u S. ( B (,) A ) C _d x = -u S. ( B (,) A ) D _d y )
5	2 4	ifeq12d	|- ( ph -> if ( A <_ B , S. ( A (,) B ) C _d x , -u S. ( B (,) A ) C _d x ) = if ( A <_ B , S. ( A (,) B ) D _d y , -u S. ( B (,) A ) D _d y ) )
6		df-ditg	|- S_ [ A -> B ] C _d x = if ( A <_ B , S. ( A (,) B ) C _d x , -u S. ( B (,) A ) C _d x )
7		df-ditg	|- S_ [ A -> B ] D _d y = if ( A <_ B , S. ( A (,) B ) D _d y , -u S. ( B (,) A ) D _d y )
8	5 6 7	3eqtr4g	|- ( ph -> S_ [ A -> B ] C _d x = S_ [ A -> B ] D _d y )