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

Theorem feqmptd 5738
Description: Deduction form of dffn5 5731. (Contributed by Mario Carneiro, 8-Jan-2015.)
Hypothesis
Ref Expression
feqmptd.1  |-  ( ph  ->  F : A --> B )
Assertion
Ref Expression
feqmptd  |-  ( ph  ->  F  =  ( x  e.  A  |->  ( F `
 x ) ) )
Distinct variable groups:    x, A    x, F
Allowed substitution hints:    ph( x)    B( x)

Proof of Theorem feqmptd
StepHypRef Expression
1 feqmptd.1 . . 3  |-  ( ph  ->  F : A --> B )
2 ffn 5550 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
31, 2syl 16 . 2  |-  ( ph  ->  F  Fn  A )
4 dffn5 5731 . 2  |-  ( F  Fn  A  <->  F  =  ( x  e.  A  |->  ( F `  x
) ) )
53, 4sylib 189 1  |-  ( ph  ->  F  =  ( x  e.  A  |->  ( F `
 x ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. cmpt 4226    Fn wfn 5408   -->wf 5409   ` cfv 5413
This theorem is referenced by:  feqresmpt  5739  fcoconst  5864  ofco  6283  caofinvl  6290  caofcom  6295  caofass  6297  caofdi  6299  caofdir  6300  caonncan  6301  suppssof1  6305  mapxpen  7232  xpmapenlem  7233  cantnfp1  7593  cantnflem1  7601  cnfcom2lem  7614  infxpenc  7855  pwfseqlem5  8494  gruf  8642  ccatco  11759  cnrecnv  11925  lo1o12  12282  rlimclim1  12294  rlimuni  12299  lo1resb  12313  rlimresb  12314  o1resb  12315  rlimcn1  12337  rlimcn1b  12338  rlimo1  12365  o1rlimmul  12367  caucvgr  12424  ackbijnn  12562  bitsf1ocnv  12911  ramcl  13352  pwsplusgval  13667  pwsmulrval  13668  pwsvscafval  13671  setcepi  14198  prf1st  14256  prf2nd  14257  1st2ndprf  14258  curfuncf  14290  curf2ndf  14299  yonedainv  14333  yonffthlem  14334  prdsidlem  14682  pwsco1mhm  14724  pwsco2mhm  14725  frmdup3  14766  grpinvcnv  14814  pwsinvg  14885  pwssub  14886  efginvrel1  15315  frgpup3lem  15364  frgpup3  15365  gsumval3  15469  gsumcllem  15471  gsumzf1o  15474  gsumzsplit  15484  gsumconst  15487  gsumzmhm  15488  gsumsub  15497  gsum2d  15501  gsumcom2  15504  dprdfadd  15533  dprdfsub  15534  dprdfeq0  15535  dprdf11  15536  dmdprdsplitlem  15550  dprddisj2  15552  dpjidcl  15571  ablfaclem2  15599  ablfac2  15602  lmhmvsca  16076  rrgsupp  16306  psrbagaddcl  16390  gsumbagdiaglem  16395  psrass1lem  16397  psrlinv  16416  psrass1  16424  psrcom  16427  mplsubrglem  16457  mplmonmul  16482  mplcoe1  16483  mplcoe2  16485  evlslem2  16523  coe1fval3  16561  coe1sclmul  16629  coe1sclmul2  16631  ply1coe  16639  mulgrhm2  16743  cygznlem2a  16803  frgpcyg  16809  neiptopnei  17151  dfac14  17603  ptcnp  17607  lmcn2  17634  cnmpt11f  17649  cnmpt21f  17657  cnmpt2k  17673  qtopeu  17701  xkocnv  17799  xkohmeo  17800  flfcnp2  17992  istgp2  18074  tmdgsum  18078  symgtgp  18084  subgtgp  18088  tgpconcomp  18095  prdstgpd  18107  tsmsmhm  18128  tsmssub  18131  tgptsmscls  18132  tsmssplit  18134  tsmsxplem1  18135  tlmtgp  18178  ustuqtop  18229  prdsmslem1  18510  prdsxmslem1  18511  prdsxmslem2  18512  tngnm  18645  nmoeq0  18723  cnfldnm  18766  cncfmpt1f  18896  negfcncf  18902  cnrehmeo  18931  evth  18937  evth2  18938  copco  18996  pcopt  19000  pcopt2  19001  pcoass  19002  pcorev2  19006  pi1xfrcnv  19035  ovolctb  19339  ovolfs2  19416  uniioombllem2  19428  uniioombllem3  19430  ismbf  19475  mbfconst  19480  ismbfcn2  19484  mbfmulc2re  19493  mbfadd  19506  mbfsub  19507  mbflimsup  19511  itg1climres  19559  mbfi1flimlem  19567  mbfi1flim  19568  mbfmul  19571  itg2uba  19588  itg2mulclem  19591  itg2mulc  19592  itg2splitlem  19593  itg2monolem1  19595  itg2i1fseq  19600  itg2gt0  19605  itg2cnlem1  19606  itg2cnlem2  19607  i1fibl  19652  itgitg1  19653  iblabslem  19672  iblabs  19673  bddmulibl  19683  cnplimc  19727  limccnp  19731  limccnp2  19732  dvcnp2  19759  dvmulf  19782  dvcmulf  19784  dvcobr  19785  dvcof  19787  dvcjbr  19788  dvcj  19789  dvfre  19790  dvmptcj  19807  dvcnvlem  19813  dvcnv  19814  dvef  19817  dvsincos  19818  rolle  19827  cmvth  19828  dvlip  19830  dvlipcn  19831  dv11cn  19838  dvivthlem1  19845  dvivth  19847  lhop2  19852  dvfsumrlim2  19869  ftc1lem1  19872  ftc1lem2  19873  ftc1a  19874  ftc1lem4  19876  ftc2  19881  ftc2ditglem  19882  ftc2ditg  19883  evlslem6  19887  evlslem1  19889  tdeglem4  19936  tdeglem2  19937  mdegle0  19953  mdegmullem  19954  plypf1  20084  plyco  20113  dgrcolem1  20144  dgrcolem2  20145  dgrco  20146  plycjlem  20147  dvply2g  20155  plydiveu  20168  elqaalem3  20191  taylthlem1  20242  taylthlem2  20243  ulmshft  20259  ulmdvlem1  20269  mtest  20273  mtestbdd  20274  mbfulm  20275  iblulm  20276  itgulm  20277  pserulm  20291  pserdv  20298  abelthlem1  20300  abelthlem3  20302  pige3  20378  eff1olem  20403  logcn  20491  advlog  20498  advlogexp  20499  logtayl  20504  logccv  20507  dvcxp1  20579  dvcxp2  20580  resqrcn  20586  sqrcn  20587  loglesqr  20595  dvatan  20728  leibpi  20735  divsqrsumo1  20775  jensenlem2  20779  amgmlem  20781  ftalem7  20814  basellem9  20824  muinv  20931  dchrmulid2  20989  dchrinvcl  20990  lgseisenlem4  21089  dchrisum0lem2a  21164  logdivsum  21180  mulog2sumlem1  21181  log2sumbnd  21191  hilnormi  22618  chscllem4  23095  hmopidmchi  23607  cofmpt  24031  ofoprabco  24032  qqhre  24339  esumpcvgval  24421  ofcfval4  24441  lgamgulmlem2  24767  lgamcvg2  24792  ptpcon  24873  cvmliftlem6  24930  cvmliftlem8  24932  cvmlift2lem7  24949  cvmliftphtlem  24957  cvmlift3lem5  24963  mblfinlem  26143  volsupnfl  26150  cnambfre  26154  itg2addnclem  26155  itg2addnclem2  26156  itg2addnclem3  26157  itg2addnc  26158  itg2gt0cn  26159  itgaddnc  26164  itgmulc2nc  26172  bddiblnc  26174  ftc1cnnclem  26177  upixp  26321  mzpsubst  26695  diophun  26722  uvcresum  27110  frlmup1  27118  psgnunilem5  27285  grpvrinv  27319  mhmvlin  27320  mendlmod  27369  mendassa  27370  cncfmptss  27584  dvsinexp  27607  itgsinexplem1  27615  stoweidlem20  27636
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-fv 5421
  Copyright terms: Public domain W3C validator