Theorem cbvdisjvw2

Description: Change bound variable and domain in a disjoint collection, using implicit substitution. (Contributed by GG, 14-Aug-2025)

	Ref	Expression
Hypotheses	cbvdisjvw2.1	$$⊢x=y\to C=D$$
	cbvdisjvw2.2	$$⊢x=y\to A=B$$
Assertion	cbvdisjvw2	$$⊢\underset{x\in A}{Disj}C\leftrightarrow \underset{y\in B}{Disj}D$$

Proof

Step	Hyp	Ref	Expression
1		cbvdisjvw2.1	$$⊢x=y\to C=D$$
2		cbvdisjvw2.2	$$⊢x=y\to A=B$$
3	1	eleq2d	$$⊢x=y\to \left(t\in C\leftrightarrow t\in D\right)$$
4	2 3	cbvrmovw2	$$⊢{\exists }^{*}x\in At\in C\leftrightarrow {\exists }^{*}y\in Bt\in D$$
5	4	albii	$$⊢\forall t{\exists }^{*}x\in At\in C\leftrightarrow \forall t{\exists }^{*}y\in Bt\in D$$
6		df-disj	$$⊢\underset{x\in A}{Disj}C\leftrightarrow \forall t{\exists }^{*}x\in At\in C$$
7		df-disj	$$⊢\underset{y\in B}{Disj}D\leftrightarrow \forall t{\exists }^{*}y\in Bt\in D$$
8	5 6 7	3bitr4i	$$⊢\underset{x\in A}{Disj}C\leftrightarrow \underset{y\in B}{Disj}D$$