dfaimafn

Description: Alternate definition of the image of a function, analogous to dfimafn . (Contributed by Alexander van der Vekens, 25-May-2017)

		Ref	Expression
	Assertion	dfaimafn	$⊢ (Fun F \land A \subseteq dom F) \to F [A] = \{y \| \exists x \in A (F''' x) = y\}$

Step	Hyp	Ref	Expression
1		dfima2	$⊢ F [A] = \{y \| \exists x \in A x F y\}$
2		ssel	$⊢ A \subseteq dom F \to (x \in A \to x \in dom F)$
3		funbrafvb	$⊢ (Fun F \land x \in dom F) \to ((F''' x) = y \leftrightarrow x F y)$
4	3	ex	$⊢ Fun F \to (x \in dom F \to ((F''' x) = y \leftrightarrow x F y))$
5	2 4	syl9r	$⊢ Fun F \to (A \subseteq dom F \to (x \in A \to ((F''' x) = y \leftrightarrow x F y)))$
6	5	imp31	$⊢ ((Fun F \land A \subseteq dom F) \land x \in A) \to ((F''' x) = y \leftrightarrow x F y)$
7	6	rexbidva	$⊢ (Fun F \land A \subseteq dom F) \to (\exists x \in A (F''' x) = y \leftrightarrow \exists x \in A x F y)$
8	7	abbidv	$⊢ (Fun F \land A \subseteq dom F) \to \{y \| \exists x \in A (F''' x) = y\} = \{y \| \exists x \in A x F y\}$
9	1 8	eqtr4id	$⊢ (Fun F \land A \subseteq dom F) \to F [A] = \{y \| \exists x \in A (F''' x) = y\}$

Metamath Proof Explorer