funbrfv2b

Description: Function value in terms of a binary relation. (Contributed by Mario Carneiro, 19-Mar-2014)

		Ref	Expression
	Assertion	funbrfv2b	$⊢ 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		funbrfvb	$⊢ (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