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

Theorem dffn5 5911
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 5677 . . . . 5  |-  ( F  Fn  A  ->  Rel  F )
2 dfrel4v 5456 . . . . 5  |-  ( Rel 
F  <->  F  =  { <. x ,  y >.  |  x F y } )
31, 2sylib 196 . . . 4  |-  ( F  Fn  A  ->  F  =  { <. x ,  y
>.  |  x F
y } )
4 fnbr 5681 . . . . . . . 8  |-  ( ( F  Fn  A  /\  x F y )  ->  x  e.  A )
54ex 434 . . . . . . 7  |-  ( F  Fn  A  ->  (
x F y  ->  x  e.  A )
)
65pm4.71rd 635 . . . . . 6  |-  ( F  Fn  A  ->  (
x F y  <->  ( x  e.  A  /\  x F y ) ) )
7 eqcom 2476 . . . . . . . 8  |-  ( y  =  ( F `  x )  <->  ( F `  x )  =  y )
8 fnbrfvb 5906 . . . . . . . 8  |-  ( ( F  Fn  A  /\  x  e.  A )  ->  ( ( F `  x )  =  y  <-> 
x F y ) )
97, 8syl5bb 257 . . . . . . 7  |-  ( ( F  Fn  A  /\  x  e.  A )  ->  ( y  =  ( F `  x )  <-> 
x F y ) )
109pm5.32da 641 . . . . . 6  |-  ( F  Fn  A  ->  (
( x  e.  A  /\  y  =  ( F `  x )
)  <->  ( x  e.  A  /\  x F y ) ) )
116, 10bitr4d 256 . . . . 5  |-  ( F  Fn  A  ->  (
x F y  <->  ( x  e.  A  /\  y  =  ( F `  x ) ) ) )
1211opabbidv 4510 . . . 4  |-  ( F  Fn  A  ->  { <. x ,  y >.  |  x F y }  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  ( F `  x ) ) } )
133, 12eqtrd 2508 . . 3  |-  ( F  Fn  A  ->  F  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  ( F `  x ) ) } )
14 df-mpt 4507 . . 3  |-  ( x  e.  A  |->  ( F `
 x ) )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  ( F `  x ) ) }
1513, 14syl6eqr 2526 . 2  |-  ( F  Fn  A  ->  F  =  ( x  e.  A  |->  ( F `  x ) ) )
16 fvex 5874 . . . 4  |-  ( F `
 x )  e. 
_V
17 eqid 2467 . . . 4  |-  ( x  e.  A  |->  ( F `
 x ) )  =  ( x  e.  A  |->  ( F `  x ) )
1816, 17fnmpti 5707 . . 3  |-  ( x  e.  A  |->  ( F `
 x ) )  Fn  A
19 fneq1 5667 . . 3  |-  ( F  =  ( x  e.  A  |->  ( F `  x ) )  -> 
( F  Fn  A  <->  ( x  e.  A  |->  ( F `  x ) )  Fn  A ) )
2018, 19mpbiri 233 . 2  |-  ( F  =  ( x  e.  A  |->  ( F `  x ) )  ->  F  Fn  A )
2115, 20impbii 188 1  |-  ( F  Fn  A  <->  F  =  ( x  e.  A  |->  ( F `  x
) ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369    = wceq 1379    e. wcel 1767   class class class wbr 4447   {copab 4504    |-> cmpt 4505   Rel wrel 5004    Fn wfn 5581   ` cfv 5586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-iota 5549  df-fun 5588  df-fn 5589  df-fv 5594
This theorem is referenced by:  fnrnfv  5912  feqmptd  5918  dffn5f  5920  eqfnfv  5973  fndmin  5986  fcompt  6055  resfunexg  6124  eufnfv  6132  nvocnv  6173  fnov  6392  offveqb  6544  caofinvl  6549  oprabco  6864  df1st2  6866  df2nd2  6867  curry1  6872  curry2  6875  resixpfo  7504  pw2f1olem  7618  marypha2lem3  7893  seqof  12128  prmrec  14295  prdsbascl  14734  xpsaddlem  14826  xpsvsca  14830  oppccatid  14971  fuclid  15189  fucrid  15190  curfuncf  15361  yonedainv  15404  yonffthlem  15405  prdsidlem  15766  pws0g  15770  prdsinvlem  15978  gsummptmhm  16754  staffn  17281  mptscmfsuppd  17360  prdslmodd  17398  ofco2  18720  1mavmul  18817  cnmpt1st  19904  cnmpt2nd  19905  ptunhmeo  20044  xpsxmetlem  20617  xpsmet  20620  itg2split  21891  pserulm  22551  pserdvlem2  22557  logcn  22756  emcllem5  23057  fcomptf  27175  pl1cn  27573  esumpcvgval  27724  eulerpartgbij  27951  dstfrvclim1  28056  plymulx0  28144  gamcvg2lem  28241  ptpcon  28318  ovoliunnfl  29633  voliunnfl  29635  dvtanlem  29641  fnopabco  29816  upixp  29823  prdsbnd  29892  prdstotbnd  29893  prdsbnd2  29894  fgraphopab  30775  expgrowthi  30838  expgrowth  30840  cncfiooicclem1  31232  dvcosre  31239  itgsubsticclem  31293  dirkercncflem2  31404  fourierdlem56  31463  fourierdlem62  31469  fourierdlem90  31497  fdmdifeqresdif  31995  offvalfv  31996
  Copyright terms: Public domain W3C validator