Metamath Proof Explorer

Theorem fnbrfvb2

Description: Version of fnbrfvb for functions on Cartesian products: function value expressed as a binary relation. See fnbrovb for the form when F is seen as a binary operation. (Contributed by BJ, 15-Feb-2022)

		Ref	Expression
	Assertion	fnbrfvb2	$⊢ (F Fn (V \times W) \land (A \in V \land B \in W)) \to (F (⟨A, B⟩) = C \leftrightarrow ⟨A, B⟩ F C)$

Proof

Step	Hyp	Ref	Expression
1		opelxpi	$⊢ (A \in V \land B \in W) \to ⟨A, B⟩ \in (V \times W)$
2		fnbrfvb	$⊢ (F Fn (V \times W) \land ⟨A, B⟩ \in (V \times W)) \to (F (⟨A, B⟩) = C \leftrightarrow ⟨A, B⟩ F C)$
3	1 2	sylan2	$⊢ (F Fn (V \times W) \land (A \in V \land B \in W)) \to (F (⟨A, B⟩) = C \leftrightarrow ⟨A, B⟩ F C)$