Theorem funressnbrafv2

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

	Ref	Expression
Assertion	funressnbrafv2	|- ( ( ( A e. V /\ B e. W ) /\ Fun ( F |` { A } ) ) -> ( A F B -> ( F '''' A ) = B ) )

Proof

Step	Hyp	Ref	Expression
1		simpllr	|- ( ( ( ( A e. V /\ B e. W ) /\ Fun ( F |` { A } ) ) /\ A F B ) -> B e. W )
2		eleq1	|- ( x = B -> ( x e. W <-> B e. W ) )
3	2	anbi2d	|- ( x = B -> ( ( A e. V /\ x e. W ) <-> ( A e. V /\ B e. W ) ) )
4	3	anbi1d	|- ( x = B -> ( ( ( A e. V /\ x e. W ) /\ Fun ( F |` { A } ) ) <-> ( ( A e. V /\ B e. W ) /\ Fun ( F |` { A } ) ) ) )
5		breq2	|- ( x = B -> ( A F x <-> A F B ) )
6	4 5	anbi12d	|- ( x = B -> ( ( ( ( A e. V /\ x e. W ) /\ Fun ( F |` { A } ) ) /\ A F x ) <-> ( ( ( A e. V /\ B e. W ) /\ Fun ( F |` { A } ) ) /\ A F B ) ) )
7		eqeq2	|- ( x = B -> ( ( F '''' A ) = x <-> ( F '''' A ) = B ) )
8	6 7	imbi12d	|- ( x = B -> ( ( ( ( ( A e. V /\ x e. W ) /\ Fun ( F |` { A } ) ) /\ A F x ) -> ( F '''' A ) = x ) <-> ( ( ( ( A e. V /\ B e. W ) /\ Fun ( F |` { A } ) ) /\ A F B ) -> ( F '''' A ) = B ) ) )
9		id	|- ( A F x -> A F x )
10		funressneu	|- ( ( ( A e. V /\ x e. W ) /\ Fun ( F |` { A } ) /\ A F x ) -> E! x A F x )
11	10	3expa	|- ( ( ( ( A e. V /\ x e. W ) /\ Fun ( F |` { A } ) ) /\ A F x ) -> E! x A F x )
12		tz6.12-1-afv2	|- ( ( A F x /\ E! x A F x ) -> ( F '''' A ) = x )
13	9 11 12	syl2an2	|- ( ( ( ( A e. V /\ x e. W ) /\ Fun ( F |` { A } ) ) /\ A F x ) -> ( F '''' A ) = x )
14	8 13	vtoclg	|- ( B e. W -> ( ( ( ( A e. V /\ B e. W ) /\ Fun ( F |` { A } ) ) /\ A F B ) -> ( F '''' A ) = B ) )
15	1 14	mpcom	|- ( ( ( ( A e. V /\ B e. W ) /\ Fun ( F |` { A } ) ) /\ A F B ) -> ( F '''' A ) = B )
16	15	ex	|- ( ( ( A e. V /\ B e. W ) /\ Fun ( F |` { A } ) ) -> ( A F B -> ( F '''' A ) = B ) )