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

Proof

Step	Hyp	Ref	Expression
1		opelxpi	\|- ( ( A e. V /\ B e. W ) -> <. A , B >. e. ( V X. W ) )
2		fnbrfvb	\|- ( ( F Fn ( V X. W ) /\ <. A , B >. e. ( V X. W ) ) -> ( ( F ` <. A , B >. ) = C <-> <. A , B >. F C ) )
3	1 2	sylan2	\|- ( ( F Fn ( V X. W ) /\ ( A e. V /\ B e. W ) ) -> ( ( F ` <. A , B >. ) = C <-> <. A , B >. F C ) )

Step

Hyp

Ref

Expression

opelxpi

 |-  ( ( A e. V /\ B e. W ) -> <. A , B >. e. ( V X. W ) )

fnbrfvb

 |-  ( ( F Fn ( V X. W ) /\ <. A , B >. e. ( V X. W ) ) -> ( ( F ` <. A , B >. ) = C <-> <. A , B >. F C ) )

1 2

sylan2

 |-  ( ( F Fn ( V X. W ) /\ ( A e. V /\ B e. W ) ) -> ( ( F ` <. A , B >. ) = C <-> <. A , B >. F C ) )