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	$$⊢\mathrm{ran}\bigcup A=\bigcup _{x\in A}\mathrm{ran}x$$

Proof

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