Theorem dfimafn2

Description: Alternate definition of the image of a function as an indexed union of singletons of function values. (Contributed by Raph Levien, 20-Nov-2006)

	Ref	Expression
Assertion	dfimafn2	$$⊢\left(\mathrm{Fun}F\wedge A\subseteq \mathrm{dom}F\right)\to F\left[A\right]=\bigcup _{x\in A}\left\{F\left(x\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dfimafn	$$⊢\left(\mathrm{Fun}F\wedge A\subseteq \mathrm{dom}F\right)\to F\left[A\right]=\left\{y|\exists x\in AF\left(x\right)=y\right\}$$
2		iunab	$$⊢\bigcup _{x\in A}\left\{y|F\left(x\right)=y\right\}=\left\{y|\exists x\in AF\left(x\right)=y\right\}$$
3	1 2	eqtr4di	$$⊢\left(\mathrm{Fun}F\wedge A\subseteq \mathrm{dom}F\right)\to F\left[A\right]=\bigcup _{x\in A}\left\{y|F\left(x\right)=y\right\}$$
4		df-sn	$$⊢\left\{F\left(x\right)\right\}=\left\{y|y=F\left(x\right)\right\}$$
5		eqcom	$$⊢y=F\left(x\right)\leftrightarrow F\left(x\right)=y$$
6	5	abbii	$$⊢\left\{y|y=F\left(x\right)\right\}=\left\{y|F\left(x\right)=y\right\}$$
7	4 6	eqtri	$$⊢\left\{F\left(x\right)\right\}=\left\{y|F\left(x\right)=y\right\}$$
8	7	a1i	$$⊢x\in A\to \left\{F\left(x\right)\right\}=\left\{y|F\left(x\right)=y\right\}$$
9	8	iuneq2i	$$⊢\bigcup _{x\in A}\left\{F\left(x\right)\right\}=\bigcup _{x\in A}\left\{y|F\left(x\right)=y\right\}$$
10	3 9	eqtr4di	$$⊢\left(\mathrm{Fun}F\wedge A\subseteq \mathrm{dom}F\right)\to F\left[A\right]=\bigcup _{x\in A}\left\{F\left(x\right)\right\}$$