Metamath Proof Explorer

Theorem funbrafv22b

Description: Equivalence of function value and binary relation, analogous to funbrfvb . (Contributed by AV, 6-Sep-2022)

		Ref	Expression
	Assertion	funbrafv22b	$⊢ (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		fnbrafv2b	$⊢ (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)$