This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rnuni

Description: The range of a union. Part of Exercise 8 of Enderton p. 41. (Contributed by NM, 17-Mar-2004) (Revised by Mario Carneiro, 29-May-2015)

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

Proof

Step	Hyp	Ref	Expression
1		uniiun	$⊢ ⋃ A = ⋃_{x \in A} x$
2	1	rneqi	$⊢ ran ⋃ A = ran ⋃_{x \in A} x$
3		rniun	$⊢ ran ⋃_{x \in A} x = ⋃_{x \in A} ran x$
4	2 3	eqtri	$⊢ ran ⋃ A = ⋃_{x \in A} ran x$