funbrafv2b

Description: Function value in terms of a binary relation, analogous to funbrfv2b . (Contributed by Alexander van der Vekens, 25-May-2017)

		Ref	Expression
	Assertion	funbrafv2b	$⊢ Fun F \to (A F B \leftrightarrow (A \in dom F \land (F''' A) = B))$

Step	Hyp	Ref	Expression
1		funrel	$⊢ Fun F \to Rel F$
2		releldm	$⊢ (Rel F \land A F B) \to A \in dom F$
3	2	ex	$⊢ Rel F \to (A F B \to A \in dom F)$
4	1 3	syl	$⊢ Fun F \to (A F B \to A \in dom F)$
5	4	pm4.71rd	$⊢ Fun F \to (A F B \leftrightarrow (A \in dom F \land A F B))$
6		funbrafvb	$⊢ (Fun F \land A \in dom F) \to ((F''' A) = B \leftrightarrow A F B)$
7	6	pm5.32da	$⊢ Fun F \to ((A \in dom F \land (F''' A) = B) \leftrightarrow (A \in dom F \land A F B))$
8	5 7	bitr4d	$⊢ Fun F \to (A F B \leftrightarrow (A \in dom F \land (F''' A) = B))$

Metamath Proof Explorer