Metamath Proof Explorer

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	$⊢ (Fun F \land A \subseteq dom F) \to F [A] = ⋃_{x \in A} \{(F''' x)\}$

Proof

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