Theorem fnbrfvb

Description: Equivalence of function value and binary relation. (Contributed by NM, 19-Apr-2004) (Revised by Mario Carneiro, 28-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( F ` B ) = ( F ` B )
2		fvex	|- ( F ` B ) e. _V
3		eqeq2	|- ( x = ( F ` B ) -> ( ( F ` B ) = x <-> ( F ` B ) = ( F ` B ) ) )
4		breq2	|- ( x = ( F ` B ) -> ( B F x <-> B F ( F ` B ) ) )
5	3 4	bibi12d	|- ( x = ( F ` B ) -> ( ( ( F ` B ) = x <-> B F x ) <-> ( ( F ` B ) = ( F ` B ) <-> B F ( F ` B ) ) ) )
6	5	imbi2d	|- ( x = ( F ` B ) -> ( ( ( F Fn A /\ B e. A ) -> ( ( F ` B ) = x <-> B F x ) ) <-> ( ( F Fn A /\ B e. A ) -> ( ( F ` B ) = ( F ` B ) <-> B F ( F ` B ) ) ) ) )
7		fneu	|- ( ( F Fn A /\ B e. A ) -> E! x B F x )
8		tz6.12c	|- ( E! x B F x -> ( ( F ` B ) = x <-> B F x ) )
9	7 8	syl	|- ( ( F Fn A /\ B e. A ) -> ( ( F ` B ) = x <-> B F x ) )
10	2 6 9	vtocl	|- ( ( F Fn A /\ B e. A ) -> ( ( F ` B ) = ( F ` B ) <-> B F ( F ` B ) ) )
11	1 10	mpbii	|- ( ( F Fn A /\ B e. A ) -> B F ( F ` B ) )
12		breq2	|- ( ( F ` B ) = C -> ( B F ( F ` B ) <-> B F C ) )
13	11 12	syl5ibcom	|- ( ( F Fn A /\ B e. A ) -> ( ( F ` B ) = C -> B F C ) )
14		fnfun	|- ( F Fn A -> Fun F )
15		funbrfv	|- ( Fun F -> ( B F C -> ( F ` B ) = C ) )
16	14 15	syl	|- ( F Fn A -> ( B F C -> ( F ` B ) = C ) )
17	16	adantr	|- ( ( F Fn A /\ B e. A ) -> ( B F C -> ( F ` B ) = C ) )
18	13 17	impbid	|- ( ( F Fn A /\ B e. A ) -> ( ( F ` B ) = C <-> B F C ) )