Metamath Proof Explorer


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