Theorem cbvdisj

Description: Change bound variables in a disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016)

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

Proof

Step	Hyp	Ref	Expression
1		cbvdisj.1	$$⊢\underset{\_}{Ⅎ}yB$$
2		cbvdisj.2	$$⊢\underset{\_}{Ⅎ}xC$$
3		cbvdisj.3	$$⊢x=y\to B=C$$
4	1	nfcri	$$⊢Ⅎyz\in B$$
5	2	nfcri	$$⊢Ⅎxz\in C$$
6	3	eleq2d	$$⊢x=y\to \left(z\in B\leftrightarrow z\in C\right)$$
7	4 5 6	cbvrmow	$$⊢{\exists }^{*}x\in Az\in B\leftrightarrow {\exists }^{*}y\in Az\in C$$
8	7	albii	$$⊢\forall z{\exists }^{*}x\in Az\in B\leftrightarrow \forall z{\exists }^{*}y\in Az\in C$$
9		df-disj	$$⊢\underset{x\in A}{Disj}B\leftrightarrow \forall z{\exists }^{*}x\in Az\in B$$
10		df-disj	$$⊢\underset{y\in A}{Disj}C\leftrightarrow \forall z{\exists }^{*}y\in Az\in C$$
11	8 9 10	3bitr4i	$$⊢\underset{x\in A}{Disj}B\leftrightarrow \underset{y\in A}{Disj}C$$