Metamath Proof Explorer

Theorem funbrafv22b

Description: Equivalence of function value and binary relation, analogous to funbrfvb . (Contributed by AV, 6-Sep-2022)

Ref Expression
Assertion funbrafv22b 
|- ( ( 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 fnbrafv2b 
 |-  ( ( 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 ) )