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 ${⊢}\left({F}Fn{A}\wedge {B}\in {A}\right)\to \left({F}\left({B}\right)={C}↔{B}{F}{C}\right)$

Proof

Step Hyp Ref Expression
1 eqid ${⊢}{F}\left({B}\right)={F}\left({B}\right)$
2 fvex ${⊢}{F}\left({B}\right)\in \mathrm{V}$
3 eqeq2 ${⊢}{x}={F}\left({B}\right)\to \left({F}\left({B}\right)={x}↔{F}\left({B}\right)={F}\left({B}\right)\right)$
4 breq2 ${⊢}{x}={F}\left({B}\right)\to \left({B}{F}{x}↔{B}{F}{F}\left({B}\right)\right)$
5 3 4 bibi12d ${⊢}{x}={F}\left({B}\right)\to \left(\left({F}\left({B}\right)={x}↔{B}{F}{x}\right)↔\left({F}\left({B}\right)={F}\left({B}\right)↔{B}{F}{F}\left({B}\right)\right)\right)$
6 5 imbi2d ${⊢}{x}={F}\left({B}\right)\to \left(\left(\left({F}Fn{A}\wedge {B}\in {A}\right)\to \left({F}\left({B}\right)={x}↔{B}{F}{x}\right)\right)↔\left(\left({F}Fn{A}\wedge {B}\in {A}\right)\to \left({F}\left({B}\right)={F}\left({B}\right)↔{B}{F}{F}\left({B}\right)\right)\right)\right)$
7 fneu ${⊢}\left({F}Fn{A}\wedge {B}\in {A}\right)\to \exists !{x}\phantom{\rule{.4em}{0ex}}{B}{F}{x}$
8 tz6.12c ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{B}{F}{x}\to \left({F}\left({B}\right)={x}↔{B}{F}{x}\right)$
9 7 8 syl ${⊢}\left({F}Fn{A}\wedge {B}\in {A}\right)\to \left({F}\left({B}\right)={x}↔{B}{F}{x}\right)$
10 2 6 9 vtocl ${⊢}\left({F}Fn{A}\wedge {B}\in {A}\right)\to \left({F}\left({B}\right)={F}\left({B}\right)↔{B}{F}{F}\left({B}\right)\right)$
11 1 10 mpbii ${⊢}\left({F}Fn{A}\wedge {B}\in {A}\right)\to {B}{F}{F}\left({B}\right)$
12 breq2 ${⊢}{F}\left({B}\right)={C}\to \left({B}{F}{F}\left({B}\right)↔{B}{F}{C}\right)$
13 11 12 syl5ibcom ${⊢}\left({F}Fn{A}\wedge {B}\in {A}\right)\to \left({F}\left({B}\right)={C}\to {B}{F}{C}\right)$
14 fnfun ${⊢}{F}Fn{A}\to \mathrm{Fun}{F}$
15 funbrfv ${⊢}\mathrm{Fun}{F}\to \left({B}{F}{C}\to {F}\left({B}\right)={C}\right)$
16 14 15 syl ${⊢}{F}Fn{A}\to \left({B}{F}{C}\to {F}\left({B}\right)={C}\right)$
17 16 adantr ${⊢}\left({F}Fn{A}\wedge {B}\in {A}\right)\to \left({B}{F}{C}\to {F}\left({B}\right)={C}\right)$
18 13 17 impbid ${⊢}\left({F}Fn{A}\wedge {B}\in {A}\right)\to \left({F}\left({B}\right)={C}↔{B}{F}{C}\right)$