This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )