Metamath Proof Explorer


Theorem cbviundavw

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

Ref Expression
Hypothesis cbviundavw.1 φ x = y B = C
Assertion cbviundavw φ x A B = y A C

Proof

Step Hyp Ref Expression
1 cbviundavw.1 φ x = y B = C
2 1 eleq2d φ x = y t B t C
3 2 cbvrexdva φ x A t B y A t C
4 3 abbidv φ t | x A t B = t | y A t C
5 df-iun x A B = t | x A t B
6 df-iun y A C = t | y A t C
7 4 5 6 3eqtr4g φ x A B = y A C