Theorem fnbrovb

Description: Value of a binary operation expressed as a binary relation. See also fnbrfvb for functions on Cartesian products. (Contributed by BJ, 15-Feb-2022)

	Ref	Expression
Assertion	fnbrovb	⊢ ( ( 𝐹 Fn ( 𝑉 × 𝑊 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( ( 𝐴 𝐹 𝐵 ) = 𝐶 ↔ ⟨ 𝐴 , 𝐵 ⟩ 𝐹 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		df-ov	⊢ ( 𝐴 𝐹 𝐵 ) = ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
2	1	eqeq1i	⊢ ( ( 𝐴 𝐹 𝐵 ) = 𝐶 ↔ ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐶 )
3		fnbrfvb2	⊢ ( ( 𝐹 Fn ( 𝑉 × 𝑊 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐶 ↔ ⟨ 𝐴 , 𝐵 ⟩ 𝐹 𝐶 ) )
4	2 3	bitrid	⊢ ( ( 𝐹 Fn ( 𝑉 × 𝑊 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( ( 𝐴 𝐹 𝐵 ) = 𝐶 ↔ ⟨ 𝐴 , 𝐵 ⟩ 𝐹 𝐶 ) )