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

Theorem dffn5 5732
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 5504 . . . . 5  |-  ( F  Fn  A  ->  Rel  F )
2 dfrel4v 5284 . . . . 5  |-  ( Rel 
F  <->  F  =  { <. x ,  y >.  |  x F y } )
31, 2sylib 196 . . . 4  |-  ( F  Fn  A  ->  F  =  { <. x ,  y
>.  |  x F
y } )
4 fnbr 5508 . . . . . . . 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 2440 . . . . . . . 8  |-  ( y  =  ( F `  x )  <->  ( F `  x )  =  y )
8 fnbrfvb 5727 . . . . . . . 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 4350 . . . 4  |-  ( F  Fn  A  ->  { <. x ,  y >.  |  x F y }  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  ( F `  x ) ) } )
133, 12eqtrd 2470 . . 3  |-  ( F  Fn  A  ->  F  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  ( F `  x ) ) } )
14 df-mpt 4347 . . 3  |-  ( x  e.  A  |->  ( F `
 x ) )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  ( F `  x ) ) }
1513, 14syl6eqr 2488 . 2  |-  ( F  Fn  A  ->  F  =  ( x  e.  A  |->  ( F `  x ) ) )
16 fvex 5696 . . . 4  |-  ( F `
 x )  e. 
_V
17 eqid 2438 . . . 4  |-  ( x  e.  A  |->  ( F `
 x ) )  =  ( x  e.  A  |->  ( F `  x ) )
1816, 17fnmpti 5534 . . 3  |-  ( x  e.  A  |->  ( F `
 x ) )  Fn  A
19 fneq1 5494 . . 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 1369    e. wcel 1756   class class class wbr 4287   {copab 4344    e. cmpt 4345   Rel wrel 4840    Fn wfn 5408   ` cfv 5413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-iota 5376  df-fun 5415  df-fn 5416  df-fv 5421
This theorem is referenced by:  fnrnfv  5733  feqmptd  5739  dffn5f  5741  eqfnfv  5792  fndmin  5805  fcompt  5874  resfunexg  5938  eufnfv  5946  nvocnv  5983  fnov  6193  offveqb  6337  caofinvl  6342  oprabco  6652  df1st2  6654  df2nd2  6655  curry1  6659  curry2  6662  resixpfo  7293  pw2f1olem  7407  marypha2lem3  7679  seqof  11855  prmrec  13975  prdsbascl  14413  xpsaddlem  14505  xpsvsca  14509  oppccatid  14650  fuclid  14868  fucrid  14869  curfuncf  15040  yonedainv  15083  yonffthlem  15084  prdsidlem  15445  pws0g  15449  prdsinvlem  15654  gsummptmhm  16426  staffn  16912  prdslmodd  17027  ofco2  18307  1mavmul  18334  cnmpt1st  19216  cnmpt2nd  19217  ptunhmeo  19356  xpsxmetlem  19929  xpsmet  19932  itg2split  21202  pserulm  21862  pserdvlem2  21868  logcn  22067  emcllem5  22368  fcomptf  25931  pl1cn  26337  esumpcvgval  26479  eulerpartgbij  26707  dstfrvclim1  26812  plymulx0  26900  gamcvg2lem  26997  ptpcon  27074  ovoliunnfl  28386  voliunnfl  28388  dvtanlem  28394  fnopabco  28569  upixp  28576  prdsbnd  28645  prdstotbnd  28646  prdsbnd2  28647  fgraphopab  29531  expgrowthi  29560  expgrowth  29562  dvcosre  29741  fdmdifeqresdif  30684  offvalfv  30685
  Copyright terms: Public domain W3C validator