Metamath Proof Explorer


Theorem funbrfv2b

Description: Function value in terms of a binary relation. (Contributed by Mario Carneiro, 19-Mar-2014)

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

Proof

Step Hyp Ref Expression
1 funrel
 |-  ( Fun F -> Rel F )
2 releldm
 |-  ( ( Rel F /\ A F B ) -> A e. dom F )
3 2 ex
 |-  ( Rel F -> ( A F B -> A e. dom F ) )
4 1 3 syl
 |-  ( Fun F -> ( A F B -> A e. dom F ) )
5 4 pm4.71rd
 |-  ( Fun F -> ( A F B <-> ( A e. dom F /\ A F B ) ) )
6 funbrfvb
 |-  ( ( Fun F /\ A e. dom F ) -> ( ( F ` A ) = B <-> A F B ) )
7 6 pm5.32da
 |-  ( Fun F -> ( ( A e. dom F /\ ( F ` A ) = B ) <-> ( A e. dom F /\ A F B ) ) )
8 5 7 bitr4d
 |-  ( Fun F -> ( A F B <-> ( A e. dom F /\ ( F ` A ) = B ) ) )