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 ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 ran 𝑥

Proof

Step	Hyp	Ref	Expression
1		uniiun	⊢ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥
2	1	rneqi	⊢ ran ∪ 𝐴 = ran ∪ 𝑥 ∈ 𝐴 𝑥
3		rniun	⊢ ran ∪ 𝑥 ∈ 𝐴 𝑥 = ∪ 𝑥 ∈ 𝐴 ran 𝑥
4	2 3	eqtri	⊢ ran ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 ran 𝑥