MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fnbrfvb Structured version   Unicode version

Theorem fnbrfvb 5729
Description: Equivalence of function value and binary relation. (Contributed by NM, 19-Apr-2004.) (Revised by Mario Carneiro, 28-Apr-2015.)
Assertion
Ref Expression
fnbrfvb  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ( ( F `  B )  =  C  <-> 
B F C ) )

Proof of Theorem fnbrfvb
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 eqid 2441 . . . 4  |-  ( F `
 B )  =  ( F `  B
)
2 fvex 5698 . . . . 5  |-  ( F `
 B )  e. 
_V
3 eqeq2 2450 . . . . . . 7  |-  ( x  =  ( F `  B )  ->  (
( F `  B
)  =  x  <->  ( F `  B )  =  ( F `  B ) ) )
4 breq2 4293 . . . . . . 7  |-  ( x  =  ( F `  B )  ->  ( B F x  <->  B F
( F `  B
) ) )
53, 4bibi12d 321 . . . . . 6  |-  ( x  =  ( F `  B )  ->  (
( ( F `  B )  =  x  <-> 
B F x )  <-> 
( ( F `  B )  =  ( F `  B )  <-> 
B F ( F `
 B ) ) ) )
65imbi2d 316 . . . . 5  |-  ( 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 5512 . . . . . 6  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  E! x  B F x )
8 tz6.12c 5706 . . . . . 6  |-  ( E! x  B F x  ->  ( ( F `
 B )  =  x  <->  B F x ) )
97, 8syl 16 . . . . 5  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ( ( F `  B )  =  x  <-> 
B F x ) )
102, 6, 9vtocl 3021 . . . 4  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ( ( F `  B )  =  ( F `  B )  <-> 
B F ( F `
 B ) ) )
111, 10mpbii 211 . . 3  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  B F ( F `
 B ) )
12 breq2 4293 . . 3  |-  ( ( F `  B )  =  C  ->  ( B F ( F `  B )  <->  B F C ) )
1311, 12syl5ibcom 220 . 2  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ( ( F `  B )  =  C  ->  B F C ) )
14 fnfun 5505 . . . 4  |-  ( F  Fn  A  ->  Fun  F )
15 funbrfv 5727 . . . 4  |-  ( Fun 
F  ->  ( B F C  ->  ( F `
 B )  =  C ) )
1614, 15syl 16 . . 3  |-  ( F  Fn  A  ->  ( B F C  ->  ( F `  B )  =  C ) )
1716adantr 462 . 2  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ( B F C  ->  ( F `  B )  =  C ) )
1813, 17impbid 191 1  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ( ( F `  B )  =  C  <-> 
B F C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1364    e. wcel 1761   E!weu 2259   class class class wbr 4289   Fun wfun 5409    Fn wfn 5410   ` cfv 5415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pr 4528
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-mo 2264  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-sbc 3184  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-br 4290  df-opab 4348  df-id 4632  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-iota 5378  df-fun 5417  df-fn 5418  df-fv 5423
This theorem is referenced by:  fnopfvb  5730  funbrfvb  5731  dffn5  5734  fnsnfv  5748  fndmdif  5804  dffo4  5856  dff13  5968  isomin  6025  isoini  6026  1stconst  6660  2ndconst  6661  fsplit  6676  seqomlem3  6903  seqomlem4  6904  nqerrel  9097  imasleval  14475  znleval  17887  axcontlem5  23133  elnlfn  25251  adjbd1o  25408  feqmptdf  25897  br1steq  27498  br2ndeq  27499  trpredpred  27605  fvbigcup  27846  fvsingle  27864  imageval  27874  brfullfun  27892  pw2f1ocnv  29295  funressnfv  29943  fnbrafvb  29969
  Copyright terms: Public domain W3C validator