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 X. W ) /\ ( A e. V /\ B e. 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 X. W ) /\ ( A e. V /\ B e. W ) ) -> ( ( F ` <. A , B >. ) = C <-> <. A , B >. F C ) )
4	2 3	bitrid	|- ( ( F Fn ( V X. W ) /\ ( A e. V /\ B e. W ) ) -> ( ( A F B ) = C <-> <. A , B >. F C ) )