Theorem fnbrafv2b

Description: Equivalence of function value and binary relation, analogous to fnbrfvb . (Contributed by AV, 6-Sep-2022)

	Ref	Expression
Assertion	fnbrafv2b	|- ( ( F Fn A /\ B e. A ) -> ( ( F '''' B ) = C <-> B F C ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( F '''' B ) = ( F '''' B )
2		fundmdfat	|- ( ( Fun F /\ B e. dom F ) -> F defAt B )
3	2	funfni	|- ( ( F Fn A /\ B e. A ) -> F defAt B )
4		dfatafv2ex	|- ( F defAt B -> ( F '''' B ) e. _V )
5	3 4	syl	|- ( ( F Fn A /\ B e. A ) -> ( F '''' B ) e. _V )
6		eqeq2	|- ( x = ( F '''' B ) -> ( ( F '''' B ) = x <-> ( F '''' B ) = ( F '''' B ) ) )
7		breq2	|- ( x = ( F '''' B ) -> ( B F x <-> B F ( F '''' B ) ) )
8	6 7	bibi12d	|- ( x = ( F '''' B ) -> ( ( ( F '''' B ) = x <-> B F x ) <-> ( ( F '''' B ) = ( F '''' B ) <-> B F ( F '''' B ) ) ) )
9	8	adantl	|- ( ( ( F Fn A /\ B e. A ) /\ x = ( F '''' B ) ) -> ( ( ( F '''' B ) = x <-> B F x ) <-> ( ( F '''' B ) = ( F '''' B ) <-> B F ( F '''' B ) ) ) )
10		fneu	|- ( ( F Fn A /\ B e. A ) -> E! x B F x )
11		tz6.12c-afv2	|- ( E! x B F x -> ( ( F '''' B ) = x <-> B F x ) )
12	10 11	syl	|- ( ( F Fn A /\ B e. A ) -> ( ( F '''' B ) = x <-> B F x ) )
13	5 9 12	vtocld	|- ( ( F Fn A /\ B e. A ) -> ( ( F '''' B ) = ( F '''' B ) <-> B F ( F '''' B ) ) )
14	1 13	mpbii	|- ( ( F Fn A /\ B e. A ) -> B F ( F '''' B ) )
15		breq2	|- ( ( F '''' B ) = C -> ( B F ( F '''' B ) <-> B F C ) )
16	14 15	syl5ibcom	|- ( ( F Fn A /\ B e. A ) -> ( ( F '''' B ) = C -> B F C ) )
17		fnfun	|- ( F Fn A -> Fun F )
18		funbrafv2	|- ( Fun F -> ( B F C -> ( F '''' B ) = C ) )
19	17 18	syl	|- ( F Fn A -> ( B F C -> ( F '''' B ) = C ) )
20	19	adantr	|- ( ( F Fn A /\ B e. A ) -> ( B F C -> ( F '''' B ) = C ) )
21	16 20	impbid	|- ( ( F Fn A /\ B e. A ) -> ( ( F '''' B ) = C <-> B F C ) )