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

Theorem feqmptd 5781
Description: Deduction form of dffn5 5774. (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 5593 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
31, 2syl 16 . 2  |-  ( ph  ->  F  Fn  A )
4 dffn5 5774 . 2  |-  ( F  Fn  A  <->  F  =  ( x  e.  A  |->  ( F `  x
) ) )
53, 4sylib 190 1  |-  ( ph  ->  F  =  ( x  e.  A  |->  ( F `
 x ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    e. cmpt 4268    Fn wfn 5451   -->wf 5452   ` cfv 5456
This theorem is referenced by:  feqresmpt  5782  fcoconst  5907  ofco  6326  caofinvl  6333  caofcom  6338  caofass  6340  caofdi  6342  caofdir  6343  caonncan  6344  suppssof1  6348  mapxpen  7275  xpmapenlem  7276  cantnfp1  7639  cantnflem1  7647  cnfcom2lem  7660  infxpenc  7901  pwfseqlem5  8540  gruf  8688  ccatco  11806  cnrecnv  11972  lo1o12  12329  rlimclim1  12341  rlimuni  12346  lo1resb  12360  rlimresb  12361  o1resb  12362  rlimcn1  12384  rlimcn1b  12385  rlimo1  12412  o1rlimmul  12414  caucvgr  12471  ackbijnn  12609  bitsf1ocnv  12958  ramcl  13399  pwsplusgval  13714  pwsmulrval  13715  pwsvscafval  13718  setcepi  14245  prf1st  14303  prf2nd  14304  1st2ndprf  14305  curfuncf  14337  curf2ndf  14346  yonedainv  14380  yonffthlem  14381  prdsidlem  14729  pwsco1mhm  14771  pwsco2mhm  14772  frmdup3  14813  grpinvcnv  14861  pwsinvg  14932  pwssub  14933  efginvrel1  15362  frgpup3lem  15411  frgpup3  15412  gsumval3  15516  gsumcllem  15518  gsumzf1o  15521  gsumzsplit  15531  gsumconst  15534  gsumzmhm  15535  gsumsub  15544  gsum2d  15548  gsumcom2  15551  dprdfadd  15580  dprdfsub  15581  dprdfeq0  15582  dprdf11  15583  dmdprdsplitlem  15597  dprddisj2  15599  dpjidcl  15618  ablfaclem2  15646  ablfac2  15649  lmhmvsca  16123  rrgsupp  16353  psrbagaddcl  16437  gsumbagdiaglem  16442  psrass1lem  16444  psrlinv  16463  psrass1  16471  psrcom  16474  mplsubrglem  16504  mplmonmul  16529  mplcoe1  16530  mplcoe2  16532  evlslem2  16570  coe1fval3  16608  coe1sclmul  16676  coe1sclmul2  16678  ply1coe  16686  mulgrhm2  16790  cygznlem2a  16850  frgpcyg  16856  neiptopnei  17198  dfac14  17652  ptcnp  17656  lmcn2  17683  cnmpt11f  17698  cnmpt21f  17706  cnmpt2k  17722  qtopeu  17750  xkocnv  17848  xkohmeo  17849  flfcnp2  18041  istgp2  18123  tmdgsum  18127  symgtgp  18133  subgtgp  18137  tgpconcomp  18144  prdstgpd  18156  tsmsmhm  18177  tsmssub  18180  tgptsmscls  18181  tsmssplit  18183  tsmsxplem1  18184  tlmtgp  18227  ustuqtop  18278  prdsmslem1  18559  prdsxmslem1  18560  prdsxmslem2  18561  tngnm  18694  nmoeq0  18772  cnfldnm  18815  cncfmpt1f  18945  negfcncf  18951  cnrehmeo  18980  evth  18986  evth2  18987  copco  19045  pcopt  19049  pcopt2  19050  pcoass  19051  pcorev2  19055  pi1xfrcnv  19084  ovolctb  19388  ovolfs2  19465  uniioombllem2  19477  uniioombllem3  19479  ismbf  19524  mbfconst  19529  ismbfcn2  19533  mbfmulc2re  19542  mbfadd  19555  mbfsub  19556  mbflimsup  19560  itg1climres  19608  mbfi1flimlem  19616  mbfi1flim  19617  mbfmul  19620  itg2uba  19637  itg2mulclem  19640  itg2mulc  19641  itg2splitlem  19642  itg2monolem1  19644  itg2i1fseq  19649  itg2gt0  19654  itg2cnlem1  19655  itg2cnlem2  19656  i1fibl  19701  itgitg1  19702  iblabslem  19721  iblabs  19722  bddmulibl  19732  cnplimc  19776  limccnp  19780  limccnp2  19781  dvcnp2  19808  dvmulf  19831  dvcmulf  19833  dvcobr  19834  dvcof  19836  dvcjbr  19837  dvcj  19838  dvfre  19839  dvmptcj  19856  dvcnvlem  19862  dvcnv  19863  dvef  19866  dvsincos  19867  rolle  19876  cmvth  19877  dvlip  19879  dvlipcn  19880  dv11cn  19887  dvivthlem1  19894  dvivth  19896  lhop2  19901  dvfsumrlim2  19918  ftc1lem1  19921  ftc1lem2  19922  ftc1a  19923  ftc1lem4  19925  ftc2  19930  ftc2ditglem  19931  ftc2ditg  19932  evlslem6  19936  evlslem1  19938  tdeglem4  19985  tdeglem2  19986  mdegle0  20002  mdegmullem  20003  plypf1  20133  plyco  20162  dgrcolem1  20193  dgrcolem2  20194  dgrco  20195  plycjlem  20196  dvply2g  20204  plydiveu  20217  elqaalem3  20240  taylthlem1  20291  taylthlem2  20292  ulmshft  20308  ulmdvlem1  20318  mtest  20322  mtestbdd  20323  mbfulm  20324  iblulm  20325  itgulm  20326  pserulm  20340  pserdv  20347  abelthlem1  20349  abelthlem3  20351  pige3  20427  eff1olem  20452  logcn  20540  advlog  20547  advlogexp  20548  logtayl  20553  logccv  20556  dvcxp1  20628  dvcxp2  20629  resqrcn  20635  sqrcn  20636  loglesqr  20644  dvatan  20777  leibpi  20784  divsqrsumo1  20824  jensenlem2  20828  amgmlem  20830  ftalem7  20863  basellem9  20873  muinv  20980  dchrmulid2  21038  dchrinvcl  21039  lgseisenlem4  21138  dchrisum0lem2a  21213  logdivsum  21229  mulog2sumlem1  21230  log2sumbnd  21240  hilnormi  22667  chscllem4  23144  hmopidmchi  23656  cofmpt  24080  ofoprabco  24081  qqhre  24388  esumpcvgval  24470  ofcfval4  24490  lgamgulmlem2  24816  lgamcvg2  24841  ptpcon  24922  cvmliftlem6  24979  cvmliftlem8  24981  cvmlift2lem7  24998  cvmliftphtlem  25006  cvmlift3lem5  25012  mblfinlem2  26246  volsupnfl  26253  cnambfre  26257  itg2addnclem  26258  itg2addnclem2  26259  itg2addnclem3  26260  itg2addnc  26261  itg2gt0cn  26262  itgaddnc  26267  itgmulc2nc  26275  bddiblnc  26277  ftc1cnnclem  26280  ftc1anclem1  26282  ftc1anclem2  26283  ftc1anclem3  26284  ftc1anclem4  26285  ftc1anclem5  26286  ftc1anclem6  26287  ftc1anclem7  26288  ftc1anclem8  26289  ftc1anc  26290  ftc2nc  26291  upixp  26433  mzpsubst  26807  diophun  26834  uvcresum  27221  frlmup1  27229  psgnunilem5  27396  grpvrinv  27430  mhmvlin  27431  mendlmod  27480  mendassa  27481  cncfmptss  27695  dvsinexp  27718  itgsinexplem1  27726  stoweidlem20  27747
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4332  ax-nul 4340  ax-pr 4405
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4215  df-opab 4269  df-mpt 4270  df-id 4500  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-iota 5420  df-fun 5458  df-fn 5459  df-f 5460  df-fv 5464
  Copyright terms: Public domain W3C validator