Theorem fniunfv

Description: The indexed union of a function's values is the union of its range. Compare Definition 5.4 of Monk1 p. 50. (Contributed by NM, 27-Sep-2004)

	Ref	Expression
Assertion	fniunfv	$$⊢FFnA\to \bigcup _{x\in A}F\left(x\right)=\bigcup \mathrm{ran}F$$

Proof

Step	Hyp	Ref	Expression
1		fvex	$$⊢F\left(x\right)\in \mathrm{V}$$
2	1	dfiun2	$$⊢\bigcup _{x\in A}F\left(x\right)=\bigcup \left\{y|\exists x\in Ay=F\left(x\right)\right\}$$
3		fnrnfv	$$⊢FFnA\to \mathrm{ran}F=\left\{y|\exists x\in Ay=F\left(x\right)\right\}$$
4	3	unieqd	$$⊢FFnA\to \bigcup \mathrm{ran}F=\bigcup \left\{y|\exists x\in Ay=F\left(x\right)\right\}$$
5	2 4	eqtr4id	$$⊢FFnA\to \bigcup _{x\in A}F\left(x\right)=\bigcup \mathrm{ran}F$$