dffn5

Description: Representation of a function in terms of its values. (Contributed by FL, 14-Sep-2013) (Proof shortened by Mario Carneiro, 31-Aug-2015)

		Ref	Expression
	Assertion	dffn5	$⊢ F Fn A \leftrightarrow F = (x \in A ⟼ F (x))$

Proof

Step	Hyp	Ref	Expression
1		fnrel	$⊢ F Fn A \to Rel F$
2		dfrel4v	$⊢ Rel F \leftrightarrow F = \{⟨x, y⟩ \| x F y\}$
3	1 2	sylib	$⊢ F Fn A \to F = \{⟨x, y⟩ \| x F y\}$
4		fnbr	$⊢ (F Fn A \land x F y) \to x \in A$
5	4	ex	$⊢ F Fn A \to (x F y \to x \in A)$
6	5	pm4.71rd	$⊢ F Fn A \to (x F y \leftrightarrow (x \in A \land x F y))$
7		eqcom	$⊢ y = F (x) \leftrightarrow F (x) = y$
8		fnbrfvb	$⊢ (F Fn A \land x \in A) \to (F (x) = y \leftrightarrow x F y)$
9	7 8	bitrid	$⊢ (F Fn A \land x \in A) \to (y = F (x) \leftrightarrow x F y)$
10	9	pm5.32da	$⊢ F Fn A \to ((x \in A \land y = F (x)) \leftrightarrow (x \in A \land x F y))$
11	6 10	bitr4d	$⊢ F Fn A \to (x F y \leftrightarrow (x \in A \land y = F (x)))$
12	11	opabbidv	$⊢ F Fn A \to \{⟨x, y⟩ \| x F y\} = \{⟨x, y⟩ \| (x \in A \land y = F (x))\}$
13	3 12	eqtrd	$⊢ F Fn A \to F = \{⟨x, y⟩ \| (x \in A \land y = F (x))\}$
14		df-mpt	$⊢ (x \in A ⟼ F (x)) = \{⟨x, y⟩ \| (x \in A \land y = F (x))\}$
15	13 14	eqtr4di	$⊢ F Fn A \to F = (x \in A ⟼ F (x))$
16		fvex	$⊢ F (x) \in V$
17		eqid	$⊢ (x \in A ⟼ F (x)) = (x \in A ⟼ F (x))$
18	16 17	fnmpti	$⊢ (x \in A ⟼ F (x)) Fn A$
19		fneq1	$⊢ F = (x \in A ⟼ F (x)) \to (F Fn A \leftrightarrow (x \in A ⟼ F (x)) Fn A)$
20	18 19	mpbiri	$⊢ F = (x \in A ⟼ F (x)) \to F Fn A$
21	15 20	impbii	$⊢ F Fn A \leftrightarrow F = (x \in A ⟼ F (x))$

Metamath Proof Explorer

Theorem dffn5

Proof