Metamath Proof Explorer

Theorem fnopfvb

Description: Equivalence of function value and ordered pair membership. (Contributed by NM, 7-Nov-1995)

Ref Expression
Assertion fnopfvb 
|- ( ( F Fn A /\ B e. A ) -> ( ( F ` B ) = C <-> <. B , C >. e. F ) )

Proof

Step Hyp Ref Expression
1 fnbrfvb 
 |-  ( ( F Fn A /\ B e. A ) -> ( ( F ` B ) = C <-> B F C ) )
2 df-br 
 |-  ( B F C <-> <. B , C >. e. F )
3 1 2 bitrdi 
 |-  ( ( F Fn A /\ B e. A ) -> ( ( F ` B ) = C <-> <. B , C >. e. F ) )