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

Theorem dffn5 5839
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 5610 . . . . 5  |-  ( F  Fn  A  ->  Rel  F )
2 dfrel4v 5390 . . . . 5  |-  ( Rel 
F  <->  F  =  { <. x ,  y >.  |  x F y } )
31, 2sylib 196 . . . 4  |-  ( F  Fn  A  ->  F  =  { <. x ,  y
>.  |  x F
y } )
4 fnbr 5614 . . . . . . . 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 2460 . . . . . . . 8  |-  ( y  =  ( F `  x )  <->  ( F `  x )  =  y )
8 fnbrfvb 5834 . . . . . . . 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 4456 . . . 4  |-  ( F  Fn  A  ->  { <. x ,  y >.  |  x F y }  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  ( F `  x ) ) } )
133, 12eqtrd 2492 . . 3  |-  ( F  Fn  A  ->  F  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  ( F `  x ) ) } )
14 df-mpt 4453 . . 3  |-  ( x  e.  A  |->  ( F `
 x ) )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  ( F `  x ) ) }
1513, 14syl6eqr 2510 . 2  |-  ( F  Fn  A  ->  F  =  ( x  e.  A  |->  ( F `  x ) ) )
16 fvex 5802 . . . 4  |-  ( F `
 x )  e. 
_V
17 eqid 2451 . . . 4  |-  ( x  e.  A  |->  ( F `
 x ) )  =  ( x  e.  A  |->  ( F `  x ) )
1816, 17fnmpti 5640 . . 3  |-  ( x  e.  A  |->  ( F `
 x ) )  Fn  A
19 fneq1 5600 . . 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 1370    e. wcel 1758   class class class wbr 4393   {copab 4450    |-> cmpt 4451   Rel wrel 4946    Fn wfn 5514   ` cfv 5519
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4514  ax-nul 4522  ax-pr 4632
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3073  df-sbc 3288  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-nul 3739  df-if 3893  df-sn 3979  df-pr 3981  df-op 3985  df-uni 4193  df-br 4394  df-opab 4452  df-mpt 4453  df-id 4737  df-xp 4947  df-rel 4948  df-cnv 4949  df-co 4950  df-dm 4951  df-iota 5482  df-fun 5521  df-fn 5522  df-fv 5527
This theorem is referenced by:  fnrnfv  5840  feqmptd  5846  dffn5f  5848  eqfnfv  5899  fndmin  5912  fcompt  5981  resfunexg  6045  eufnfv  6053  nvocnv  6090  fnov  6301  offveqb  6445  caofinvl  6450  oprabco  6760  df1st2  6762  df2nd2  6763  curry1  6767  curry2  6770  resixpfo  7404  pw2f1olem  7518  marypha2lem3  7791  seqof  11973  prmrec  14094  prdsbascl  14532  xpsaddlem  14624  xpsvsca  14628  oppccatid  14769  fuclid  14987  fucrid  14988  curfuncf  15159  yonedainv  15202  yonffthlem  15203  prdsidlem  15564  pws0g  15568  prdsinvlem  15774  gsummptmhm  16550  staffn  17049  mptscmfsuppd  17127  prdslmodd  17165  ofco2  18452  1mavmul  18479  cnmpt1st  19366  cnmpt2nd  19367  ptunhmeo  19506  xpsxmetlem  20079  xpsmet  20082  itg2split  21353  pserulm  22013  pserdvlem2  22019  logcn  22218  emcllem5  22519  fcomptf  26124  pl1cn  26523  esumpcvgval  26665  eulerpartgbij  26892  dstfrvclim1  26997  plymulx0  27085  gamcvg2lem  27182  ptpcon  27259  ovoliunnfl  28574  voliunnfl  28576  dvtanlem  28582  fnopabco  28757  upixp  28764  prdsbnd  28833  prdstotbnd  28834  prdsbnd2  28835  fgraphopab  29719  expgrowthi  29748  expgrowth  29750  dvcosre  29929  fdmdifeqresdif  30873  offvalfv  30874
  Copyright terms: Public domain W3C validator