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 ) |
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 ) |