Metamath Proof Explorer

Theorem dfafn5a

Description: Representation of a function in terms of its values, analogous to dffn5 (only one direction of implication!). (Contributed by Alexander van der Vekens, 25-May-2017)

		Ref	Expression
	Assertion	dfafn5a	$⊢ F Fn A \to 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		fnbrafvb	$⊢ (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))$