Theorem cbviindavw

Description: Change bound variable in indexed intersections. Deduction form. (Contributed by GG, 14-Aug-2025)

	Ref	Expression
Hypothesis	cbviindavw.1	|- ( ( ph /\ x = y ) -> B = C )
Assertion	cbviindavw	|- ( ph -> |^|_ x e. A B = |^|_ y e. A C )

Proof

Step	Hyp	Ref	Expression
1		cbviindavw.1	|- ( ( ph /\ x = y ) -> B = C )
2	1	eleq2d	|- ( ( ph /\ x = y ) -> ( t e. B <-> t e. C ) )
3	2	cbvraldva	|- ( ph -> ( A. x e. A t e. B <-> A. y e. A t e. C ) )
4	3	abbidv	|- ( ph -> { t | A. x e. A t e. B } = { t | A. y e. A t e. C } )
5		df-iin	|- |^|_ x e. A B = { t | A. x e. A t e. B }
6		df-iin	|- |^|_ y e. A C = { t | A. y e. A t e. C }
7	4 5 6	3eqtr4g	|- ( ph -> |^|_ x e. A B = |^|_ y e. A C )