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 )