Metamath Proof Explorer


Theorem cbviinv

Description: Change bound variables in an indexed intersection. (Contributed by Jeff Hankins, 26-Aug-2009) Add disjoint variable condition to avoid ax-13 . See cbviinvg for a less restrictive version requiring more axioms. (Revised by GG, 14-Aug-2025)

Ref Expression
Hypothesis cbviunv.1 x = y B = C
Assertion cbviinv 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 cbvralvw x A z B y A z C
4 3 abbii z | x A z B = z | y A z C
5 df-iin x A B = z | x A z B
6 df-iin y A C = z | y A z C
7 4 5 6 3eqtr4i x A B = y A C