This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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