# 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 ) )`
` |-  ( ( F Fn A /\ B e. A ) -> ( B F C -> ( F ` B ) = C ) )`
` |-  ( ( F Fn A /\ B e. A ) -> ( ( F ` B ) = C <-> B F C ) )`