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

Theorem dffn5 5568
Description: Representation of a function in terms of its values. (Contributed by FL, 14-Sep-2013.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
Assertion
Ref Expression
dffn5  |-  ( F  Fn  A  <->  F  =  ( x  e.  A  |->  ( F `  x
) ) )
Distinct variable groups:    x, A    x, F

Proof of Theorem dffn5
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 fnrel 5342 . . . . 5  |-  ( F  Fn  A  ->  Rel  F )
2 dfrel4v 5125 . . . . 5  |-  ( Rel 
F  <->  F  =  { <. x ,  y >.  |  x F y } )
31, 2sylib 188 . . . 4  |-  ( F  Fn  A  ->  F  =  { <. x ,  y
>.  |  x F
y } )
4 fnbr 5346 . . . . . . . 8  |-  ( ( F  Fn  A  /\  x F y )  ->  x  e.  A )
54ex 423 . . . . . . 7  |-  ( F  Fn  A  ->  (
x F y  ->  x  e.  A )
)
65pm4.71rd 616 . . . . . 6  |-  ( F  Fn  A  ->  (
x F y  <->  ( x  e.  A  /\  x F y ) ) )
7 eqcom 2285 . . . . . . . 8  |-  ( y  =  ( F `  x )  <->  ( F `  x )  =  y )
8 fnbrfvb 5563 . . . . . . . 8  |-  ( ( F  Fn  A  /\  x  e.  A )  ->  ( ( F `  x )  =  y  <-> 
x F y ) )
97, 8syl5bb 248 . . . . . . 7  |-  ( ( F  Fn  A  /\  x  e.  A )  ->  ( y  =  ( F `  x )  <-> 
x F y ) )
109pm5.32da 622 . . . . . 6  |-  ( F  Fn  A  ->  (
( x  e.  A  /\  y  =  ( F `  x )
)  <->  ( x  e.  A  /\  x F y ) ) )
116, 10bitr4d 247 . . . . 5  |-  ( F  Fn  A  ->  (
x F y  <->  ( x  e.  A  /\  y  =  ( F `  x ) ) ) )
1211opabbidv 4082 . . . 4  |-  ( F  Fn  A  ->  { <. x ,  y >.  |  x F y }  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  ( F `  x ) ) } )
133, 12eqtrd 2315 . . 3  |-  ( F  Fn  A  ->  F  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  ( F `  x ) ) } )
14 df-mpt 4079 . . 3  |-  ( x  e.  A  |->  ( F `
 x ) )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  ( F `  x ) ) }
1513, 14syl6eqr 2333 . 2  |-  ( F  Fn  A  ->  F  =  ( x  e.  A  |->  ( F `  x ) ) )
16 fvex 5539 . . . 4  |-  ( F `
 x )  e. 
_V
17 eqid 2283 . . . 4  |-  ( x  e.  A  |->  ( F `
 x ) )  =  ( x  e.  A  |->  ( F `  x ) )
1816, 17fnmpti 5372 . . 3  |-  ( x  e.  A  |->  ( F `
 x ) )  Fn  A
19 fneq1 5333 . . 3  |-  ( F  =  ( x  e.  A  |->  ( F `  x ) )  -> 
( F  Fn  A  <->  ( x  e.  A  |->  ( F `  x ) )  Fn  A ) )
2018, 19mpbiri 224 . 2  |-  ( F  =  ( x  e.  A  |->  ( F `  x ) )  ->  F  Fn  A )
2115, 20impbii 180 1  |-  ( F  Fn  A  <->  F  =  ( x  e.  A  |->  ( F `  x
) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    = wceq 1623    e. wcel 1684   class class class wbr 4023   {copab 4076    e. cmpt 4077   Rel wrel 4694    Fn wfn 5250   ` cfv 5255
This theorem is referenced by:  fnrnfv  5569  feqmptd  5575  dffn5f  5577  eqfnfv  5622  fndmin  5632  fcompt  5694  resfunexg  5737  eufnfv  5752  fnov  5952  offveqb  6099  caofinvl  6104  oprabco  6203  df1st2  6205  df2nd2  6206  curry1  6210  curry2  6213  resixpfo  6854  pw2f1olem  6966  marypha2lem3  7190  seqof  11103  prmrec  12969  prdsbascl  13382  xpsaddlem  13477  xpsvsca  13481  oppccatid  13622  fuclid  13840  fucrid  13841  curfuncf  14012  yonedainv  14055  yonffthlem  14056  prdsidlem  14404  pws0g  14408  prdsinvlem  14603  staffn  15614  prdslmodd  15726  cnmpt1st  17362  cnmpt2nd  17363  ptunhmeo  17499  xpsxmetlem  17943  xpsmet  17946  itg2split  19104  pserulm  19798  pserdvlem2  19804  logcn  19994  emcllem5  20293  fcomptf  23230  esumpcvgval  23446  dstfrvclim1  23678  ptpcon  23764  fnovpop  25038  fnopabco2b  25371  fnopabco  26388  upixp  26403  prdsbnd  26517  prdstotbnd  26518  prdsbnd2  26519  fgraphopab  27529  expgrowthi  27550  expgrowth  27552  dvcosre  27741  stoweidlem20  27769
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-iota 5219  df-fun 5257  df-fn 5258  df-fv 5263
  Copyright terms: Public domain W3C validator