Metamath Proof Explorer


Theorem cbviin

Description: Change bound variables in an indexed intersection. (Contributed by Jeff Hankins, 26-Aug-2009) (Revised by Mario Carneiro, 14-Oct-2016) Add disjoint variable condition to avoid ax-13 . See cbviing for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024)

Ref Expression
Hypotheses cbviun.1 _ y B
cbviun.2 _ x C
cbviun.3 x = y B = C
Assertion cbviin x A B = y A C

Proof

Step Hyp Ref Expression
1 cbviun.1 _ y B
2 cbviun.2 _ x C
3 cbviun.3 x = y B = C
4 1 nfcri y z B
5 2 nfcri x z C
6 3 eleq2d x = y z B z C
7 4 5 6 cbvralw x A z B y A z C
8 7 abbii z | x A z B = z | y A z C
9 df-iin x A B = z | x A z B
10 df-iin y A C = z | y A z C
11 8 9 10 3eqtr4i x A B = y A C