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