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