This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )