Metamath Proof Explorer

Theorem funfvbrb

Description: Two ways to say that A is in the domain of F . (Contributed by Mario Carneiro, 1-May-2014)

Ref Expression
Assertion funfvbrb 
|- ( Fun F -> ( A e. dom F <-> A F ( F ` A ) ) )

Proof

Step Hyp Ref Expression
1 funfvop 
 |-  ( ( Fun F /\ A e. dom F ) -> <. A , ( F ` A ) >. e. F )
2 df-br 
 |-  ( A F ( F ` A ) <-> <. A , ( F ` A ) >. e. F )
3 1 2 sylibr 
 |-  ( ( Fun F /\ A e. dom F ) -> A F ( F ` A ) )
4 funrel 
 |-  ( Fun F -> Rel F )
5 releldm 
 |-  ( ( Rel F /\ A F ( F ` A ) ) -> A e. dom F )
6 4 5 sylan 
 |-  ( ( Fun F /\ A F ( F ` A ) ) -> A e. dom F )
7 3 6 impbida 
 |-  ( Fun F -> ( A e. dom F <-> A F ( F ` A ) ) )