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

Metamath Proof Explorer

Theorem cbvdisjf

Description: Change bound variables in a disjoint collection. (Contributed by Thierry Arnoux, 6-Apr-2017)

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

Proof

Step Hyp Ref Expression
1 cbvdisjf.1 
 |-  F/_ x A
2 cbvdisjf.2 
 |-  F/_ y B
3 cbvdisjf.3 
 |-  F/_ x C
4 cbvdisjf.4 
 |-  ( x = y -> B = C )
5 nfv 
 |-  F/ y x e. A
6 2 nfcri 
 |-  F/ y z e. B
7 5 6 nfan 
 |-  F/ y ( x e. A /\ z e. B )
8 1 nfcri 
 |-  F/ x y e. A
9 3 nfcri 
 |-  F/ x z e. C
10 8 9 nfan 
 |-  F/ x ( y e. A /\ z e. C )
11 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
12 4 eleq2d 
 |-  ( x = y -> ( z e. B <-> z e. C ) )
13 11 12 anbi12d 
 |-  ( x = y -> ( ( x e. A /\ z e. B ) <-> ( y e. A /\ z e. C ) ) )
14 7 10 13 cbvmow 
 |-  ( E* x ( x e. A /\ z e. B ) <-> E* y ( y e. A /\ z e. C ) )
15 df-rmo 
 |-  ( E* x e. A z e. B <-> E* x ( x e. A /\ z e. B ) )
16 df-rmo 
 |-  ( E* y e. A z e. C <-> E* y ( y e. A /\ z e. C ) )
17 14 15 16 3bitr4i 
 |-  ( E* x e. A z e. B <-> E* y e. A z e. C )
18 17 albii 
 |-  ( A. z E* x e. A z e. B <-> A. z E* y e. A z e. C )
19 df-disj 
 |-  ( Disj_ x e. A B <-> A. z E* x e. A z e. B )
20 df-disj 
 |-  ( Disj_ y e. A C <-> A. z E* y e. A z e. C )
21 18 19 20 3bitr4i 
 |-  ( Disj_ x e. A B <-> Disj_ y e. A C )