dfimafn

Description: Alternate definition of the image of a function. (Contributed by Raph Levien, 20-Nov-2006)

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

Step	Hyp	Ref	Expression
1		ssel	$⊢ A \subseteq dom F \to (x \in A \to x \in dom F)$
2		funbrfvb	$⊢ (Fun F \land x \in dom F) \to (F (x) = y \leftrightarrow x F y)$
3	2	ex	$⊢ Fun F \to (x \in dom F \to (F (x) = y \leftrightarrow x F y))$
4	1 3	syl9r	$⊢ Fun F \to (A \subseteq dom F \to (x \in A \to (F (x) = y \leftrightarrow x F y)))$
5	4	imp31	$⊢ ((Fun F \land A \subseteq dom F) \land x \in A) \to (F (x) = y \leftrightarrow x F y)$
6	5	rexbidva	$⊢ (Fun F \land A \subseteq dom F) \to (\exists x \in A F (x) = y \leftrightarrow \exists x \in A x F y)$
7	6	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\}$
8		dfima2	$⊢ F [A] = \{y \| \exists x \in A x F y\}$
9	7 8	syl6reqr	$⊢ (Fun F \land A \subseteq dom F) \to F [A] = \{y \| \exists x \in A F (x) = y\}$

Metamath Proof Explorer