Metamath Proof Explorer

Theorem funopfvb

Description: Equivalence of function value and ordered pair membership. Theorem 4.3(ii) of Monk1 p. 42. (Contributed by NM, 26-Jan-1997)

Ref Expression
Assertion funopfvb 
|- ( ( Fun F /\ A e. dom F ) -> ( ( F ` A ) = B <-> <. A , B >. e. F ) )

Proof

Step Hyp Ref Expression
1 funfn 
 |-  ( Fun F <-> F Fn dom F )
2 fnopfvb 
 |-  ( ( F Fn dom F /\ A e. dom F ) -> ( ( F ` A ) = B <-> <. A , B >. e. F ) )
3 1 2 sylanb 
 |-  ( ( Fun F /\ A e. dom F ) -> ( ( F ` A ) = B <-> <. A , B >. e. F ) )