Theorem dfaimafn2

Description: Alternate definition of the image of a function as an indexed union of singletons of function values, analogous to dfimafn2 . (Contributed by Alexander van der Vekens, 25-May-2017)

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

Proof

Step	Hyp	Ref	Expression
1		dfaimafn	$$⊢\left(\mathrm{Fun}F\wedge A\subseteq \mathrm{dom}F\right)\to F\left[A\right]=\left\{y|\exists x\in A\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)=y\right\}$$
2		iunab	$$⊢\bigcup _{x\in A}\left\{y|\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)=y\right\}=\left\{y|\exists x\in A\left(F\mathrm{\text{'}\text{'}\text{'}}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|\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)=y\right\}$$
4		df-sn	$$⊢\left\{\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\right\}=\left\{y|y=\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\right\}$$
5		eqcom	$$⊢y=\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\leftrightarrow \left(F\mathrm{\text{'}\text{'}\text{'}}x\right)=y$$
6	5	abbii	$$⊢\left\{y|y=\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\right\}=\left\{y|\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)=y\right\}$$
7	4 6	eqtri	$$⊢\left\{\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\right\}=\left\{y|\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)=y\right\}$$
8	7	a1i	$$⊢x\in A\to \left\{\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\right\}=\left\{y|\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)=y\right\}$$
9	8	iuneq2i	$$⊢\bigcup _{x\in A}\left\{\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\right\}=\bigcup _{x\in A}\left\{y|\left(F\mathrm{\text{'}\text{'}\text{'}}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\{\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\right\}$$