Metamath Proof Explorer

Theorem funbrafvb

Description: Equivalence of function value and binary relation, analogous to funbrfvb . (Contributed by Alexander van der Vekens, 25-May-2017)

Ref Expression
Assertion funbrafvb 
|- ( ( 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 fnbrafvb 
 |-  ( ( 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 ) )