rniun

Description: The range of an indexed union. (Contributed by Mario Carneiro, 29-May-2015)

		Ref	Expression
	Assertion	rniun	$⊢ ran ⋃_{x \in A} B = ⋃_{x \in A} ran B$

Step	Hyp	Ref	Expression
1		rexcom4	$⊢ \exists x \in A \exists y ⟨y, z⟩ \in B \leftrightarrow \exists y \exists x \in A ⟨y, z⟩ \in B$
2		vex	$⊢ z \in V$
3	2	elrn2	$⊢ z \in ran B \leftrightarrow \exists y ⟨y, z⟩ \in B$
4	3	rexbii	$⊢ \exists x \in A z \in ran B \leftrightarrow \exists x \in A \exists y ⟨y, z⟩ \in B$
5		eliun	$⊢ ⟨y, z⟩ \in ⋃_{x \in A} B \leftrightarrow \exists x \in A ⟨y, z⟩ \in B$
6	5	exbii	$⊢ \exists y ⟨y, z⟩ \in ⋃_{x \in A} B \leftrightarrow \exists y \exists x \in A ⟨y, z⟩ \in B$
7	1 4 6	3bitr4ri	$⊢ \exists y ⟨y, z⟩ \in ⋃_{x \in A} B \leftrightarrow \exists x \in A z \in ran B$
8	2	elrn2	$⊢ z \in ran ⋃_{x \in A} B \leftrightarrow \exists y ⟨y, z⟩ \in ⋃_{x \in A} B$
9		eliun	$⊢ z \in ⋃_{x \in A} ran B \leftrightarrow \exists x \in A z \in ran B$
10	7 8 9	3bitr4i	$⊢ z \in ran ⋃_{x \in A} B \leftrightarrow z \in ⋃_{x \in A} ran B$
11	10	eqriv	$⊢ ran ⋃_{x \in A} B = ⋃_{x \in A} ran B$

Metamath Proof Explorer