Theorem disjrdx

Description: Re-index a disjunct collection statement. (Contributed by Thierry Arnoux, 7-Apr-2017)

	Ref	Expression
Hypotheses	disjrdx.1	$$⊢\phi \to F:A\underset{1-1\; onto}{⟶}C$$
	disjrdx.2	$$⊢\left(\phi \wedge y=F\left(x\right)\right)\to D=B$$
Assertion	disjrdx	$$⊢\phi \to \left(\underset{x\in A}{Disj}B\leftrightarrow \underset{y\in C}{Disj}D\right)$$

Proof

Step	Hyp	Ref	Expression
1		disjrdx.1	$$⊢\phi \to F:A\underset{1-1\; onto}{⟶}C$$
2		disjrdx.2	$$⊢\left(\phi \wedge y=F\left(x\right)\right)\to D=B$$
3		f1of	$$⊢F:A\underset{1-1\; onto}{⟶}C\to F:A⟶C$$
4	1 3	syl	$$⊢\phi \to F:A⟶C$$
5	4	ffvelcdmda	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)\in C$$
6		f1ofveu	$$⊢\left(F:A\underset{1-1\; onto}{⟶}C\wedge y\in C\right)\to \exists !x\in AF\left(x\right)=y$$
7	1 6	sylan	$$⊢\left(\phi \wedge y\in C\right)\to \exists !x\in AF\left(x\right)=y$$
8		eqcom	$$⊢F\left(x\right)=y\leftrightarrow y=F\left(x\right)$$
9	8	reubii	$$⊢\exists !x\in AF\left(x\right)=y\leftrightarrow \exists !x\in Ay=F\left(x\right)$$
10	7 9	sylib	$$⊢\left(\phi \wedge y\in C\right)\to \exists !x\in Ay=F\left(x\right)$$
11	2	eleq2d	$$⊢\left(\phi \wedge y=F\left(x\right)\right)\to \left(z\in D\leftrightarrow z\in B\right)$$
12	5 10 11	rmoxfrd	$$⊢\phi \to \left({\exists }^{*}y\in Cz\in D\leftrightarrow {\exists }^{*}x\in Az\in B\right)$$
13	12	bicomd	$$⊢\phi \to \left({\exists }^{*}x\in Az\in B\leftrightarrow {\exists }^{*}y\in Cz\in D\right)$$
14	13	albidv	$$⊢\phi \to \left(\forall z{\exists }^{*}x\in Az\in B\leftrightarrow \forall z{\exists }^{*}y\in Cz\in D\right)$$
15		df-disj	$$⊢\underset{x\in A}{Disj}B\leftrightarrow \forall z{\exists }^{*}x\in Az\in B$$
16		df-disj	$$⊢\underset{y\in C}{Disj}D\leftrightarrow \forall z{\exists }^{*}y\in Cz\in D$$
17	14 15 16	3bitr4g	$$⊢\phi \to \left(\underset{x\in A}{Disj}B\leftrightarrow \underset{y\in C}{Disj}D\right)$$