Metamath Proof Explorer

Theorem funbrafv

Description: The second argument of a binary relation on a function is the function's value, analogous to funbrfv . (Contributed by Alexander van der Vekens, 25-May-2017)

Ref Expression
Assertion funbrafv 
|- ( Fun F -> ( A F B -> ( 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 funbrafvb 
 |-  ( ( Fun F /\ A e. dom F ) -> ( ( F ''' A ) = B <-> A F B ) )
4 3 biimprd 
 |-  ( ( Fun F /\ A e. dom F ) -> ( A F B -> ( F ''' A ) = B ) )
5 4 expcom 
 |-  ( A e. dom F -> ( Fun F -> ( A F B -> ( F ''' A ) = B ) ) )
6 2 5 syl 
 |-  ( ( Rel F /\ A F B ) -> ( Fun F -> ( A F B -> ( F ''' A ) = B ) ) )
7 6 ex 
 |-  ( Rel F -> ( A F B -> ( Fun F -> ( A F B -> ( F ''' A ) = B ) ) ) )
8 7 com14 
 |-  ( A F B -> ( A F B -> ( Fun F -> ( Rel F -> ( F ''' A ) = B ) ) ) )
9 8 pm2.43i 
 |-  ( A F B -> ( Fun F -> ( Rel F -> ( F ''' A ) = B ) ) )
10 9 com13 
 |-  ( Rel F -> ( Fun F -> ( A F B -> ( F ''' A ) = B ) ) )
11 1 10 syl 
 |-  ( Fun F -> ( Fun F -> ( A F B -> ( F ''' A ) = B ) ) )
12 11 pm2.43i 
 |-  ( Fun F -> ( A F B -> ( F ''' A ) = B ) )