disjrdx

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

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

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

Metamath Proof Explorer