Theorem funbrafv2

Description: The second argument of a binary relation on a function is the function's value, analogous to funbrfv . (Contributed by AV, 6-Sep-2022)

	Ref	Expression
Assertion	funbrafv2	|- ( 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	|- ( x = B -> ( A F x <-> A F B ) )
5	4	anbi2d	|- ( x = B -> ( ( Fun F /\ A F x ) <-> ( Fun F /\ A F B ) ) )
6		eqeq2	|- ( x = B -> ( ( F '''' A ) = x <-> ( F '''' A ) = B ) )
7	5 6	imbi12d	|- ( x = B -> ( ( ( Fun F /\ A F x ) -> ( F '''' A ) = x ) <-> ( ( Fun F /\ A F B ) -> ( F '''' A ) = B ) ) )
8		funeu	|- ( ( Fun F /\ A F x ) -> E! x A F x )
9		tz6.12-1-afv2	|- ( ( A F x /\ E! x A F x ) -> ( F '''' A ) = x )
10	8 9	sylan2	|- ( ( A F x /\ ( Fun F /\ A F x ) ) -> ( F '''' A ) = x )
11	10	anabss7	|- ( ( Fun F /\ A F x ) -> ( F '''' A ) = x )
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 ) )