# Metamath Proof Explorer

## Theorem funbrfv

Description: The second argument of a binary relation on a function is the function's value. (Contributed by NM, 30-Apr-2004) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion funbrfv
`|- ( Fun F -> ( A F B -> ( F ` A ) = B ) )`

### Proof

Step Hyp Ref Expression
1 funrel
` |-  ( Fun F -> Rel F )`
2 brrelex2
` |-  ( ( Rel F /\ A F B ) -> B e. _V )`
3 1 2 sylan
` |-  ( ( Fun F /\ A F B ) -> B e. _V )`
4 breq2
` |-  ( y = B -> ( A F y <-> A F B ) )`
5 4 anbi2d
` |-  ( y = B -> ( ( Fun F /\ A F y ) <-> ( Fun F /\ A F B ) ) )`
6 eqeq2
` |-  ( y = B -> ( ( F ` A ) = y <-> ( F ` A ) = B ) )`
7 5 6 imbi12d
` |-  ( y = B -> ( ( ( Fun F /\ A F y ) -> ( F ` A ) = y ) <-> ( ( Fun F /\ A F B ) -> ( F ` A ) = B ) ) )`
8 funeu
` |-  ( ( Fun F /\ A F y ) -> E! y A F y )`
9 tz6.12-1
` |-  ( ( A F y /\ E! y A F y ) -> ( F ` A ) = y )`
10 8 9 sylan2
` |-  ( ( A F y /\ ( Fun F /\ A F y ) ) -> ( F ` A ) = y )`
11 10 anabss7
` |-  ( ( Fun F /\ A F y ) -> ( F ` A ) = y )`
12 7 11 vtoclg
` |-  ( B e. _V -> ( ( Fun F /\ A F B ) -> ( F ` A ) = B ) )`
13 3 12 mpcom
` |-  ( ( Fun F /\ A F B ) -> ( F ` A ) = B )`
14 13 ex
` |-  ( Fun F -> ( A F B -> ( F ` A ) = B ) )`