Metamath Proof Explorer

Theorem funbrafvb

Description: Equivalence of function value and binary relation, analogous to funbrfvb . (Contributed by Alexander van der Vekens, 25-May-2017)

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

Step	Hyp	Ref	Expression
1		funfn	$⊢ Fun F \leftrightarrow F Fn dom F$
2		fnbrafvb	$⊢ (F Fn dom F \land A \in dom F) \to ((F''' A) = B \leftrightarrow A F B)$
3	1 2	sylanb	$⊢ (Fun F \land A \in dom F) \to ((F''' A) = B \leftrightarrow A F B)$