Metamath Proof Explorer


Theorem cbviunv

Description: Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by NM, 15-Sep-2003) Add disjoint variable condition to avoid ax-13 . See cbviunvg for a less restrictive version requiring more axioms. (Revised by GG, 14-Aug-2025)

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

Proof

Step Hyp Ref Expression
1 cbviunv.1 x = y B = C
2 1 eleq2d x = y z B z C
3 2 cbvrexvw x A z B y A z C
4 3 abbii z | x A z B = z | y A z C
5 df-iun x A B = z | x A z B
6 df-iun y A C = z | y A z C
7 4 5 6 3eqtr4i x A B = y A C