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		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		funbrfvb	$⊢ (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