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	⊢ ( ( 𝐹 Fn ( 𝑉 × 𝑊 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐶 ↔ ⟨ 𝐴 , 𝐵 ⟩ 𝐹 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		opelxpi	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑉 × 𝑊 ) )
2		fnbrfvb	⊢ ( ( 𝐹 Fn ( 𝑉 × 𝑊 ) ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑉 × 𝑊 ) ) → ( ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐶 ↔ ⟨ 𝐴 , 𝐵 ⟩ 𝐹 𝐶 ) )
3	1 2	sylan2	⊢ ( ( 𝐹 Fn ( 𝑉 × 𝑊 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐶 ↔ ⟨ 𝐴 , 𝐵 ⟩ 𝐹 𝐶 ) )