Metamath Proof Explorer

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 ⊢ F Fn V × W ∧ A ∈ V ∧ B ∈ W → A F B = C ↔ A B F C

Proof

Step Hyp Ref Expression
1 df-ov ⊢ A F B = F ⁡ A B
2 1 eqeq1i ⊢ A F B = C ↔ F ⁡ A B = C
3 fnbrfvb2 ⊢ F Fn V × W ∧ A ∈ V ∧ B ∈ W → F ⁡ A B = C ↔ A B F C
4 2 3 bitrid ⊢ F Fn V × W ∧ A ∈ V ∧ B ∈ W → A F B = C ↔ A B F C