imaiun1

Description: The image of an indexed union is the indexed union of the images. (Contributed by RP, 29-Jun-2020)

		Ref	Expression
	Assertion	imaiun1	$⊢ ⋃_{x \in A} B [C] = ⋃_{x \in A} B [C]$

Step	Hyp	Ref	Expression
1		rexcom4	$⊢ \exists x \in A \exists z (z \in C \land ⟨z, y⟩ \in B) \leftrightarrow \exists z \exists x \in A (z \in C \land ⟨z, y⟩ \in B)$
2		vex	$⊢ y \in V$
3	2	elima3	$⊢ y \in B [C] \leftrightarrow \exists z (z \in C \land ⟨z, y⟩ \in B)$
4	3	rexbii	$⊢ \exists x \in A y \in B [C] \leftrightarrow \exists x \in A \exists z (z \in C \land ⟨z, y⟩ \in B)$
5		eliun	$⊢ ⟨z, y⟩ \in ⋃_{x \in A} B \leftrightarrow \exists x \in A ⟨z, y⟩ \in B$
6	5	anbi2i	$⊢ (z \in C \land ⟨z, y⟩ \in ⋃_{x \in A} B) \leftrightarrow (z \in C \land \exists x \in A ⟨z, y⟩ \in B)$
7		r19.42v	$⊢ \exists x \in A (z \in C \land ⟨z, y⟩ \in B) \leftrightarrow (z \in C \land \exists x \in A ⟨z, y⟩ \in B)$
8	6 7	bitr4i	$⊢ (z \in C \land ⟨z, y⟩ \in ⋃_{x \in A} B) \leftrightarrow \exists x \in A (z \in C \land ⟨z, y⟩ \in B)$
9	8	exbii	$⊢ \exists z (z \in C \land ⟨z, y⟩ \in ⋃_{x \in A} B) \leftrightarrow \exists z \exists x \in A (z \in C \land ⟨z, y⟩ \in B)$
10	1 4 9	3bitr4ri	$⊢ \exists z (z \in C \land ⟨z, y⟩ \in ⋃_{x \in A} B) \leftrightarrow \exists x \in A y \in B [C]$
11	2	elima3	$⊢ y \in ⋃_{x \in A} B [C] \leftrightarrow \exists z (z \in C \land ⟨z, y⟩ \in ⋃_{x \in A} B)$
12		eliun	$⊢ y \in ⋃_{x \in A} B [C] \leftrightarrow \exists x \in A y \in B [C]$
13	10 11 12	3bitr4i	$⊢ y \in ⋃_{x \in A} B [C] \leftrightarrow y \in ⋃_{x \in A} B [C]$
14	13	eqriv	$⊢ ⋃_{x \in A} B [C] = ⋃_{x \in A} B [C]$

Metamath Proof Explorer