Theorem cbviundavw

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

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

Proof

Step	Hyp	Ref	Expression
1		cbviundavw.1	|- ( ( ph /\ x = y ) -> B = C )
2	1	eleq2d	|- ( ( ph /\ x = y ) -> ( t e. B <-> t e. C ) )
3	2	cbvrexdva	|- ( ph -> ( E. x e. A t e. B <-> E. y e. A t e. C ) )
4	3	abbidv	|- ( ph -> { t | E. x e. A t e. B } = { t | E. y e. A t e. C } )
5		df-iun	|- U_ x e. A B = { t | E. x e. A t e. B }
6		df-iun	|- U_ y e. A C = { t | E. y e. A t e. C }
7	4 5 6	3eqtr4g	|- ( ph -> U_ x e. A B = U_ y e. A C )