Metamath Proof Explorer

Theorem fnotaovb

Description: Equivalence of operation value and ordered triple membership, analogous to fnopfvb . (Contributed by Alexander van der Vekens, 26-May-2017)

Ref Expression
Assertion fnotaovb 
|- ( ( 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 opelxpi 
 |-  ( ( C e. A /\ D e. B ) -> <. C , D >. e. ( A X. B ) )
2 fnopafvb 
 |-  ( ( F Fn ( A X. B ) /\ <. C , D >. e. ( A X. B ) ) -> ( ( F ''' <. C , D >. ) = R <-> <. <. C , D >. , R >. e. F ) )
3 1 2 sylan2 
 |-  ( ( F Fn ( A X. B ) /\ ( C e. A /\ D e. B ) ) -> ( ( F ''' <. C , D >. ) = R <-> <. <. C , D >. , R >. e. F ) )
4 3 3impb 
 |-  ( ( F Fn ( A X. B ) /\ C e. A /\ D e. B ) -> ( ( F ''' <. C , D >. ) = R <-> <. <. C , D >. , R >. e. F ) )
5 df-aov 
 |-  (( C F D )) = ( F ''' <. C , D >. )
6 5 eqeq1i 
 |-  ( (( C F D )) = R <-> ( F ''' <. C , D >. ) = R )
7 df-ot 
 |-  <. C , D , R >. = <. <. C , D >. , R >.
8 7 eleq1i 
 |-  ( <. C , D , R >. e. F <-> <. <. C , D >. , R >. e. F )
9 4 6 8 3bitr4g 
 |-  ( ( F Fn ( A X. B ) /\ C e. A /\ D e. B ) -> ( (( C F D )) = R <-> <. C , D , R >. e. F ) )