This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cbvdisj

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

Ref Expression
Hypotheses cbvdisj.1 
|- F/_ y B
cbvdisj.2 
|- F/_ x C
cbvdisj.3 
|- ( x = y -> B = C )
Assertion cbvdisj 
|- ( Disj_ x e. A B <-> Disj_ y e. A C )

Proof

Step Hyp Ref Expression
1 cbvdisj.1 
 |-  F/_ y B
2 cbvdisj.2 
 |-  F/_ x C
3 cbvdisj.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 cbvrmow 
 |-  ( E* x e. A z e. B <-> E* y e. A z e. C )
8 7 albii 
 |-  ( A. z E* x e. A z e. B <-> A. z E* y e. A z e. C )
9 df-disj 
 |-  ( Disj_ x e. A B <-> A. z E* x e. A z e. B )
10 df-disj 
 |-  ( Disj_ y e. A C <-> A. z E* y e. A z e. C )
11 8 9 10 3bitr4i 
 |-  ( Disj_ x e. A B <-> Disj_ y e. A C )