Theorem fnotovb

Description: Equivalence of operation value and ordered triple membership, analogous to fnopfvb . (Contributed by NM, 17-Dec-2008) (Revised by Mario Carneiro, 28-Apr-2015) (Proof shortened by BJ, 15-Feb-2022)

	Ref	Expression
Assertion	fnotovb	|- ( ( F Fn ( A X. B ) /\ C e. A /\ D e. B ) -> ( ( C F D ) = R <-> <. C , D , R >. e. F ) )

Proof

Step	Hyp	Ref	Expression
1		fnbrovb	|- ( ( F Fn ( A X. B ) /\ ( C e. A /\ D e. B ) ) -> ( ( C F D ) = R <-> <. C , D >. F R ) )
2		df-br	|- ( <. C , D >. F R <-> <. <. C , D >. , R >. e. F )
3	2	a1i	|- ( ( F Fn ( A X. B ) /\ ( C e. A /\ D e. B ) ) -> ( <. C , D >. F R <-> <. <. C , D >. , R >. e. F ) )
4		df-ot	|- <. C , D , R >. = <. <. C , D >. , R >.
5	4	eqcomi	|- <. <. C , D >. , R >. = <. C , D , R >.
6	5	eleq1i	|- ( <. <. C , D >. , R >. e. F <-> <. C , D , R >. e. F )
7	6	a1i	|- ( ( F Fn ( A X. B ) /\ ( C e. A /\ D e. B ) ) -> ( <. <. C , D >. , R >. e. F <-> <. C , D , R >. e. F ) )
8	1 3 7	3bitrd	|- ( ( F Fn ( A X. B ) /\ ( C e. A /\ D e. B ) ) -> ( ( C F D ) = R <-> <. C , D , R >. e. F ) )
9	8	3impb	|- ( ( F Fn ( A X. B ) /\ C e. A /\ D e. B ) -> ( ( C F D ) = R <-> <. C , D , R >. e. F ) )