Metamath Proof Explorer

Theorem funbrfvb

Description: Equivalence of function value and binary relation. (Contributed by NM, 26-Mar-2006)

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

Proof

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