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 )