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

Theorem funbrfv 5644
Description: The second argument of a binary relation on a function is the function's value. (Contributed by NM, 30-Apr-2004.) (Revised by Mario Carneiro, 28-Apr-2015.)
Assertion
Ref Expression
funbrfv  |-  ( Fun 
F  ->  ( A F B  ->  ( F `
 A )  =  B ) )

Proof of Theorem funbrfv
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 funrel 5354 . . . 4  |-  ( Fun 
F  ->  Rel  F )
2 brrelex2 4810 . . . 4  |-  ( ( Rel  F  /\  A F B )  ->  B  e.  _V )
31, 2sylan 457 . . 3  |-  ( ( Fun  F  /\  A F B )  ->  B  e.  _V )
4 breq2 4108 . . . . . 6  |-  ( y  =  B  ->  ( A F y  <->  A F B ) )
54anbi2d 684 . . . . 5  |-  ( y  =  B  ->  (
( Fun  F  /\  A F y )  <->  ( Fun  F  /\  A F B ) ) )
6 eqeq2 2367 . . . . 5  |-  ( y  =  B  ->  (
( F `  A
)  =  y  <->  ( F `  A )  =  B ) )
75, 6imbi12d 311 . . . 4  |-  ( y  =  B  ->  (
( ( Fun  F  /\  A F y )  ->  ( F `  A )  =  y )  <->  ( ( Fun 
F  /\  A F B )  ->  ( F `  A )  =  B ) ) )
8 funeu 5360 . . . . . 6  |-  ( ( Fun  F  /\  A F y )  ->  E! y  A F
y )
9 tz6.12-1 5627 . . . . . 6  |-  ( ( A F y  /\  E! y  A F
y )  ->  ( F `  A )  =  y )
108, 9sylan2 460 . . . . 5  |-  ( ( A F y  /\  ( Fun  F  /\  A F y ) )  ->  ( F `  A )  =  y )
1110anabss7 794 . . . 4  |-  ( ( Fun  F  /\  A F y )  -> 
( F `  A
)  =  y )
127, 11vtoclg 2919 . . 3  |-  ( B  e.  _V  ->  (
( Fun  F  /\  A F B )  -> 
( F `  A
)  =  B ) )
133, 12mpcom 32 . 2  |-  ( ( Fun  F  /\  A F B )  ->  ( F `  A )  =  B )
1413ex 423 1  |-  ( Fun 
F  ->  ( A F B  ->  ( F `
 A )  =  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1642    e. wcel 1710   E!weu 2209   _Vcvv 2864   class class class wbr 4104   Rel wrel 4776   Fun wfun 5331   ` cfv 5337
This theorem is referenced by:  funopfv  5645  fnbrfvb  5646  fvelima  5657  fvi  5662  fmptco  5774  fliftfun  5898  fliftval  5902  opabiota  6380  fpwwe2  8355  nqerid  8647  sum0  12291  sumz  12292  fsumsers  12298  isumclim  12317  dvadd  19393  dvmul  19394  dvco  19400  dvcj  19403  dvrec  19408  dvcnv  19428  dvef  19431  ftc1cn  19494  ulmdv  19886  minvecolem4b  21571  minvecolem4  21573  hlimuni  21932  chscllem4  22333  fmptcof2  23280  cnextfvval  23502  ntrivcvgfvn0  24528  ntrivcvgtail  24529  zprodn0  24566  iprodclim  24605  fvtransport  25214  fvray  25323  fvline  25326  ftc1cnnc  25514
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4222  ax-nul 4230  ax-pr 4295
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-sbc 3068  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3909  df-br 4105  df-opab 4159  df-id 4391  df-xp 4777  df-rel 4778  df-cnv 4779  df-co 4780  df-dm 4781  df-iota 5301  df-fun 5339  df-fv 5345
  Copyright terms: Public domain W3C validator