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

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