Metamath Proof Explorer


Theorem cbviing

Description: Change bound variables in an indexed intersection. Usage of this theorem is discouraged because it depends on ax-13 . See cbviin for a version with more disjoint variable conditions, but not requiring ax-13 . (Contributed by Jeff Hankins, 26-Aug-2009) (Revised by Mario Carneiro, 14-Oct-2016) (New usage is discouraged.)

Ref Expression
Hypotheses cbviung.1
|- F/_ y B
cbviung.2
|- F/_ x C
cbviung.3
|- ( x = y -> B = C )
Assertion cbviing
|- |^|_ x e. A B = |^|_ y e. A C

Proof

Step Hyp Ref Expression
1 cbviung.1
 |-  F/_ y B
2 cbviung.2
 |-  F/_ x C
3 cbviung.3
 |-  ( x = y -> B = C )
4 1 nfcri
 |-  F/ y z e. B
5 2 nfcri
 |-  F/ x z e. C
6 3 eleq2d
 |-  ( x = y -> ( z e. B <-> z e. C ) )
7 4 5 6 cbvral
 |-  ( A. x e. A z e. B <-> A. y e. A z e. C )
8 7 abbii
 |-  { z | A. x e. A z e. B } = { z | A. y e. A z e. C }
9 df-iin
 |-  |^|_ x e. A B = { z | A. x e. A z e. B }
10 df-iin
 |-  |^|_ y e. A C = { z | A. y e. A z e. C }
11 8 9 10 3eqtr4i
 |-  |^|_ x e. A B = |^|_ y e. A C