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

Theorem dffn5 5893
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 5661 . . . . 5  |-  ( F  Fn  A  ->  Rel  F )
2 dfrel4v 5442 . . . . 5  |-  ( Rel 
F  <->  F  =  { <. x ,  y >.  |  x F y } )
31, 2sylib 196 . . . 4  |-  ( F  Fn  A  ->  F  =  { <. x ,  y
>.  |  x F
y } )
4 fnbr 5665 . . . . . . . 8  |-  ( ( F  Fn  A  /\  x F y )  ->  x  e.  A )
54ex 432 . . . . . . 7  |-  ( F  Fn  A  ->  (
x F y  ->  x  e.  A )
)
65pm4.71rd 633 . . . . . 6  |-  ( F  Fn  A  ->  (
x F y  <->  ( x  e.  A  /\  x F y ) ) )
7 eqcom 2463 . . . . . . . 8  |-  ( y  =  ( F `  x )  <->  ( F `  x )  =  y )
8 fnbrfvb 5888 . . . . . . . 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 639 . . . . . 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 4502 . . . 4  |-  ( F  Fn  A  ->  { <. x ,  y >.  |  x F y }  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  ( F `  x ) ) } )
133, 12eqtrd 2495 . . 3  |-  ( F  Fn  A  ->  F  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  ( F `  x ) ) } )
14 df-mpt 4499 . . 3  |-  ( x  e.  A  |->  ( F `
 x ) )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  ( F `  x ) ) }
1513, 14syl6eqr 2513 . 2  |-  ( F  Fn  A  ->  F  =  ( x  e.  A  |->  ( F `  x ) ) )
16 fvex 5858 . . . 4  |-  ( F `
 x )  e. 
_V
17 eqid 2454 . . . 4  |-  ( x  e.  A  |->  ( F `
 x ) )  =  ( x  e.  A  |->  ( F `  x ) )
1816, 17fnmpti 5691 . . 3  |-  ( x  e.  A  |->  ( F `
 x ) )  Fn  A
19 fneq1 5651 . . 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 367    = wceq 1398    e. wcel 1823   class class class wbr 4439   {copab 4496    |-> cmpt 4497   Rel wrel 4993    Fn wfn 5565   ` cfv 5570
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-iota 5534  df-fun 5572  df-fn 5573  df-fv 5578
This theorem is referenced by:  fnrnfv  5894  feqmptd  5901  dffn5f  5903  eqfnfv  5957  fndmin  5970  fcompt  6043  resfunexg  6112  eufnfv  6121  nvocnv  6162  fnov  6383  offveqb  6535  caofinvl  6540  oprabco  6857  df1st2  6859  df2nd2  6860  curry1  6865  curry2  6868  resixpfo  7500  pw2f1olem  7614  marypha2lem3  7889  seqof  12149  prmrec  14527  prdsbascl  14975  xpsaddlem  15067  xpsvsca  15071  oppccatid  15210  fuclid  15457  fucrid  15458  curfuncf  15709  yonedainv  15752  yonffthlem  15753  prdsidlem  16154  pws0g  16158  prdsinvlem  16380  gsummptmhm  17164  staffn  17696  prdslmodd  17813  ofco2  19123  1mavmul  19220  cnmpt1st  20338  cnmpt2nd  20339  ptunhmeo  20478  xpsxmetlem  21051  xpsmet  21054  itg2split  22325  pserulm  22986  pserdvlem2  22992  logcn  23199  logblog  23334  emcllem5  23530  fcomptf  27728  gsummpt2d  28009  pl1cn  28175  esumpcvgval  28310  esumcvgsum  28320  eulerpartgbij  28578  dstfrvclim1  28683  gamcvg2lem  28868  ptpcon  28945  ovoliunnfl  30299  voliunnfl  30301  dvtanlem  30307  fnopabco  30456  upixp  30463  prdsbnd  30532  prdstotbnd  30533  prdsbnd2  30534  fgraphopab  31414  expgrowthi  31482  expgrowth  31484  uzmptshftfval  31495  dvcosre  31948  fourierdlem56  32187  fourierdlem62  32193  fdmdifeqresdif  33204  offvalfv  33205
  Copyright terms: Public domain W3C validator