Metamath Proof Explorer


Theorem cbvdisjv

Description: Change bound variables in a disjoint collection. (Contributed by Mario Carneiro, 11-Dec-2016)

Ref Expression
Hypothesis cbvdisjv.1
|- ( x = y -> B = C )
Assertion cbvdisjv
|- ( Disj_ x e. A B <-> Disj_ y e. A C )

Proof

Step Hyp Ref Expression
1 cbvdisjv.1
 |-  ( x = y -> B = C )
2 1 eleq2d
 |-  ( x = y -> ( z e. B <-> z e. C ) )
3 2 cbvrmovw
 |-  ( E* x e. A z e. B <-> E* y e. A z e. C )
4 3 albii
 |-  ( A. z E* x e. A z e. B <-> A. z E* y e. A z e. C )
5 df-disj
 |-  ( Disj_ x e. A B <-> A. z E* x e. A z e. B )
6 df-disj
 |-  ( Disj_ y e. A C <-> A. z E* y e. A z e. C )
7 4 5 6 3bitr4i
 |-  ( Disj_ x e. A B <-> Disj_ y e. A C )