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

Theorem feqmptd 5591
Description: Deduction form of dffn5 5584. (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 5405 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
31, 2syl 15 . 2  |-  ( ph  ->  F  Fn  A )
4 dffn5 5584 . 2  |-  ( F  Fn  A  <->  F  =  ( x  e.  A  |->  ( F `  x
) ) )
53, 4sylib 188 1  |-  ( ph  ->  F  =  ( x  e.  A  |->  ( F `
 x ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    e. cmpt 4093    Fn wfn 5266   -->wf 5267   ` cfv 5271
This theorem is referenced by:  feqresmpt  5592  fcoconst  5711  ofco  6113  caofinvl  6120  caofcom  6125  caofass  6127  caofdi  6129  caofdir  6130  caonncan  6131  suppssof1  6135  mapxpen  7043  xpmapenlem  7044  cantnfp1  7399  cantnflem1  7407  cnfcom2lem  7420  infxpenc  7661  pwfseqlem5  8301  gruf  8449  ccatco  11506  cnrecnv  11666  lo1o12  12023  rlimclim1  12035  rlimuni  12040  lo1resb  12054  rlimresb  12055  o1resb  12056  rlimcn1  12078  rlimcn1b  12079  rlimo1  12106  o1rlimmul  12108  caucvgr  12164  ackbijnn  12302  bitsf1ocnv  12651  ramcl  13092  pwsplusgval  13405  pwsmulrval  13406  pwsvscafval  13409  setcepi  13936  prf1st  13994  prf2nd  13995  1st2ndprf  13996  curfuncf  14028  curf2ndf  14037  yonedainv  14071  yonffthlem  14072  prdsidlem  14420  pwsco1mhm  14462  pwsco2mhm  14463  frmdup3  14504  grpinvcnv  14552  pwsinvg  14623  pwssub  14624  efginvrel1  15053  frgpup3lem  15102  frgpup3  15103  gsumval3  15207  gsumcllem  15209  gsumzf1o  15212  gsumzsplit  15222  gsumconst  15225  gsumzmhm  15226  gsumsub  15235  gsum2d  15239  gsumcom2  15242  dprdfadd  15271  dprdfsub  15272  dprdfeq0  15273  dprdf11  15274  dmdprdsplitlem  15288  dprddisj2  15290  dpjidcl  15309  ablfaclem2  15337  ablfac2  15340  lmhmvsca  15818  rrgsupp  16048  psrbagaddcl  16132  gsumbagdiaglem  16137  psrass1lem  16139  psrlinv  16158  psrass1  16166  psrcom  16169  mplsubrglem  16199  mplmonmul  16224  mplcoe1  16225  mplcoe2  16227  evlslem2  16265  coe1fval3  16305  coe1sclmul  16374  coe1sclmul2  16376  ply1coe  16384  mulgrhm2  16477  cygznlem2a  16537  frgpcyg  16543  dfac14  17328  ptcnp  17332  lmcn2  17359  cnmpt11f  17374  cnmpt21f  17382  cnmpt2k  17398  qtopeu  17423  xkocnv  17521  xkohmeo  17522  flfcnp2  17718  istgp2  17790  tmdgsum  17794  symgtgp  17800  subgtgp  17804  tgpconcomp  17811  prdstgpd  17823  tsmsmhm  17844  tsmssub  17847  tgptsmscls  17848  tsmssplit  17850  tsmsxplem1  17851  tlmtgp  17894  prdsmslem1  18089  prdsxmslem1  18090  prdsxmslem2  18091  tngnm  18183  nmoeq0  18261  cnfldnm  18304  cncfmpt1f  18433  negfcncf  18438  cnrehmeo  18467  evth  18473  evth2  18474  copco  18532  pcopt  18536  pcopt2  18537  pcoass  18538  pcorev2  18542  pi1xfrcnv  18571  ovolctb  18865  ovolfs2  18942  uniioombllem2  18954  uniioombllem3  18956  ismbf  19001  mbfconst  19006  ismbfcn2  19010  mbfmulc2re  19019  mbfadd  19032  mbfsub  19033  mbflimsup  19037  itg1climres  19085  mbfi1flimlem  19093  mbfi1flim  19094  mbfmul  19097  itg2uba  19114  itg2mulclem  19117  itg2mulc  19118  itg2splitlem  19119  itg2monolem1  19121  itg2i1fseq  19126  itg2gt0  19131  itg2cnlem1  19132  itg2cnlem2  19133  i1fibl  19178  itgitg1  19179  iblabslem  19198  iblabs  19199  bddmulibl  19209  cnplimc  19253  limccnp  19257  limccnp2  19258  dvcnp2  19285  dvmulbr  19304  dvmulf  19308  dvcmulf  19310  dvcobr  19311  dvcof  19313  dvcjbr  19314  dvcj  19315  dvfre  19316  dvmptcj  19333  dvcnvlem  19339  dvcnv  19340  dvef  19343  dvsincos  19344  rolle  19353  cmvth  19354  dvlip  19356  dvlipcn  19357  dv11cn  19364  dvivthlem1  19371  dvivth  19373  lhop2  19378  dvfsumrlim2  19395  ftc1lem1  19398  ftc1lem2  19399  ftc1a  19400  ftc1lem4  19402  ftc2  19407  ftc2ditglem  19408  ftc2ditg  19409  evlslem6  19413  evlslem1  19415  tdeglem4  19462  tdeglem2  19463  mdegle0  19479  mdegmullem  19480  plypf1  19610  plyco  19639  dgrcolem1  19670  dgrcolem2  19671  dgrco  19672  plycjlem  19673  dvply2g  19681  plydiveu  19694  elqaalem3  19717  taylthlem1  19768  taylthlem2  19769  ulmshft  19785  ulmdvlem1  19793  mtest  19797  mbfulm  19798  iblulm  19799  itgulm  19800  pserulm  19814  pserdv  19821  abelthlem1  19823  abelthlem3  19825  pige3  19901  eff1olem  19926  logcn  20010  advlog  20017  advlogexp  20018  logtayl  20023  logccv  20026  dvcxp1  20098  dvcxp2  20099  resqrcn  20105  sqrcn  20106  loglesqr  20114  dvatan  20247  leibpi  20254  divsqrsumo1  20294  jensenlem2  20298  amgmlem  20300  ftalem7  20332  basellem9  20342  muinv  20449  dchrmulid2  20507  dchrinvcl  20508  lgseisenlem4  20607  dchrisum0lem2a  20682  logdivsum  20698  mulog2sumlem1  20699  log2sumbnd  20709  hilnormi  21758  chscllem4  22235  hmopidmchi  22747  cofmpt  23246  ofoprabco  23247  esumpcvgval  23461  ofcfval4  23481  ptpcon  23779  cvmliftlem6  23836  cvmliftlem8  23838  cvmlift2lem7  23855  cvmliftphtlem  23863  cvmlift3lem5  23869  itg2addnclem2  25004  itg2addnc  25005  itg2gt0cn  25006  itgaddnc  25011  itgmulc2nc  25019  bddiblnc  25021  ftc1cnnclem  25024  curgrpact  25475  ltrcmp  25508  addidv2  25760  issubrv  25775  mulone  25788  upixp  26506  mzpsubst  26929  diophun  26956  uvcresum  27345  frlmup1  27353  psgnunilem5  27520  grpvrinv  27554  mhmvlin  27555  mendlmod  27604  mendassa  27605  cncfmptss  27820  dvsinexp  27843  itgsinexplem1  27851
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-sbc 3005  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-opab 4094  df-mpt 4095  df-id 4325  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-fv 5279
  Copyright terms: Public domain W3C validator