Theorem cbvdisjf

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

	Ref	Expression
Hypotheses	cbvdisjf.1	$$⊢\underset{\_}{Ⅎ}xA$$
	cbvdisjf.2	$$⊢\underset{\_}{Ⅎ}yB$$
	cbvdisjf.3	$$⊢\underset{\_}{Ⅎ}xC$$
	cbvdisjf.4	$$⊢x=y\to B=C$$
Assertion	cbvdisjf	$$⊢\underset{x\in A}{Disj}B\leftrightarrow \underset{y\in A}{Disj}C$$

Proof

Step	Hyp	Ref	Expression
1		cbvdisjf.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		cbvdisjf.2	$$⊢\underset{\_}{Ⅎ}yB$$
3		cbvdisjf.3	$$⊢\underset{\_}{Ⅎ}xC$$
4		cbvdisjf.4	$$⊢x=y\to B=C$$
5		nfv	$$⊢Ⅎyx\in A$$
6	2	nfcri	$$⊢Ⅎyz\in B$$
7	5 6	nfan	$$⊢Ⅎy\left(x\in A\wedge z\in B\right)$$
8	1	nfcri	$$⊢Ⅎxy\in A$$
9	3	nfcri	$$⊢Ⅎxz\in C$$
10	8 9	nfan	$$⊢Ⅎx\left(y\in A\wedge z\in C\right)$$
11		eleq1w	$$⊢x=y\to \left(x\in A\leftrightarrow y\in A\right)$$
12	4	eleq2d	$$⊢x=y\to \left(z\in B\leftrightarrow z\in C\right)$$
13	11 12	anbi12d	$$⊢x=y\to \left(\left(x\in A\wedge z\in B\right)\leftrightarrow \left(y\in A\wedge z\in C\right)\right)$$
14	7 10 13	cbvmow	$$⊢{\exists }^{*}x\left(x\in A\wedge z\in B\right)\leftrightarrow {\exists }^{*}y\left(y\in A\wedge z\in C\right)$$
15		df-rmo	$$⊢{\exists }^{*}x\in Az\in B\leftrightarrow {\exists }^{*}x\left(x\in A\wedge z\in B\right)$$
16		df-rmo	$$⊢{\exists }^{*}y\in Az\in C\leftrightarrow {\exists }^{*}y\left(y\in A\wedge z\in C\right)$$
17	14 15 16	3bitr4i	$$⊢{\exists }^{*}x\in Az\in B\leftrightarrow {\exists }^{*}y\in Az\in C$$
18	17	albii	$$⊢\forall z{\exists }^{*}x\in Az\in B\leftrightarrow \forall z{\exists }^{*}y\in Az\in C$$
19		df-disj	$$⊢\underset{x\in A}{Disj}B\leftrightarrow \forall z{\exists }^{*}x\in Az\in B$$
20		df-disj	$$⊢\underset{y\in A}{Disj}C\leftrightarrow \forall z{\exists }^{*}y\in Az\in C$$
21	18 19 20	3bitr4i	$$⊢\underset{x\in A}{Disj}B\leftrightarrow \underset{y\in A}{Disj}C$$