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 U. A = U_ x e. A ran x

Proof

Step	Hyp	Ref	Expression
1		uniiun	|- U. A = U_ x e. A x
2	1	rneqi	|- ran U. A = ran U_ x e. A x
3		rniun	|- ran U_ x e. A x = U_ x e. A ran x
4	2 3	eqtri	|- ran U. A = U_ x e. A ran x