iunrdx

Description: Re-index an indexed union. (Contributed by Thierry Arnoux, 6-Apr-2017)

Step	Hyp	Ref	Expression
1		iunrdx.1	$⊢ φ \to F : A \underset{onto}{⟶} C$
2		iunrdx.2	$⊢ (φ \land y = F (x)) \to D = B$
3		fof	$⊢ F : A \underset{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		foelrn	$⊢ (F : A \underset{onto}{⟶} C \land y \in C) \to \exists x \in A y = F (x)$
7	1 6	sylan	$⊢ (φ \land y \in C) \to \exists x \in A y = F (x)$
8	2	eleq2d	$⊢ (φ \land y = F (x)) \to (z \in D \leftrightarrow z \in B)$
9	5 7 8	rexxfrd	$⊢ φ \to (\exists y \in C z \in D \leftrightarrow \exists x \in A z \in B)$
10	9	bicomd	$⊢ φ \to (\exists x \in A z \in B \leftrightarrow \exists y \in C z \in D)$
11	10	abbidv	$⊢ φ \to \{z \| \exists x \in A z \in B\} = \{z \| \exists y \in C z \in D\}$
12		df-iun	$⊢ ⋃_{x \in A} B = \{z \| \exists x \in A z \in B\}$
13		df-iun	$⊢ ⋃_{y \in C} D = \{z \| \exists y \in C z \in D\}$
14	11 12 13	3eqtr4g	$⊢ φ \to ⋃_{x \in A} B = ⋃_{y \in C} D$

Metamath Proof Explorer