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

Theorem feqmptd 5908
Description: Deduction form of dffn5 5900. (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 5718 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
31, 2syl 16 . 2  |-  ( ph  ->  F  Fn  A )
4 dffn5 5900 . 2  |-  ( F  Fn  A  <->  F  =  ( x  e.  A  |->  ( F `  x
) ) )
53, 4sylib 196 1  |-  ( ph  ->  F  =  ( x  e.  A  |->  ( F `
 x ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1381    |-> cmpt 4492    Fn wfn 5570   -->wf 5571   ` cfv 5575
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4555  ax-nul 4563  ax-pr 4673
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-sbc 3312  df-dif 3462  df-un 3464  df-in 3466  df-ss 3473  df-nul 3769  df-if 3924  df-sn 4012  df-pr 4014  df-op 4018  df-uni 4232  df-br 4435  df-opab 4493  df-mpt 4494  df-id 4782  df-xp 4992  df-rel 4993  df-cnv 4994  df-co 4995  df-dm 4996  df-iota 5538  df-fun 5577  df-fn 5578  df-f 5579  df-fv 5583
This theorem is referenced by:  feqresmpt  5909  fcoconst  6050  suppssof1OLD  6541  ofco  6542  caofinvl  6549  caofcom  6554  caofass  6556  caofdi  6558  caofdir  6559  caonncan  6560  suppssof1  6932  mapxpen  7682  xpmapenlem  7683  cantnfp1  8100  cantnflem1  8108  cantnfp1OLD  8126  cantnflem1OLD  8131  cnfcom2lem  8145  cnfcom2lemOLD  8153  infxpenc  8395  infxpencOLD  8400  pwfseqlem5  9041  gruf  9189  ccatco  12777  cnrecnv  12974  lo1o12  13332  rlimclim1  13344  rlimuni  13349  lo1resb  13363  rlimresb  13364  o1resb  13365  rlimcn1  13387  rlimcn1b  13388  rlimo1  13415  o1rlimmul  13417  caucvgr  13474  ackbijnn  13616  bitsf1ocnv  13968  ramcl  14421  pwsplusgval  14761  pwsmulrval  14762  pwsvscafval  14765  setcepi  15286  prf1st  15344  prf2nd  15345  1st2ndprf  15346  curfuncf  15378  curf2ndf  15387  yonedainv  15421  yonffthlem  15422  prdsidlem  15823  pwsco1mhm  15872  pwsco2mhm  15873  frmdup3lem  15905  frmdup3  15906  grpinvcnv  15977  pwsinvg  16053  pwssub  16054  psgnunilem5  16390  efginvrel1  16617  frgpup3lem  16666  frgpup3  16667  gsumval3OLD  16779  gsumval3  16782  gsumcllem  16783  gsumcllemOLD  16784  gsumzf1o  16788  gsumzf1oOLD  16791  gsumzsplit  16815  gsumzsplitOLD  16816  gsumconst  16825  gsumzmhm  16828  gsumzmhmOLD  16829  gsumsub  16845  gsumsubOLD  16846  gsum2dlem2  16869  gsum2dOLD  16871  gsumcom2  16874  dprdfadd  16931  dprdfsub  16932  dprdfeq0  16933  dprdf11  16934  dprdfaddOLD  16938  dprdfsubOLD  16939  dprdfeq0OLD  16940  dprdf11OLD  16941  dmdprdsplitlem  16955  dmdprdsplitlemOLD  16956  dprddisj2  16958  dprddisj2OLD  16959  dpjidcl  16978  dpjidclOLD  16985  ablfaclem2  17008  ablfac2  17011  mptscmfsuppd  17448  lmhmvsca  17562  rrgsupp  17810  rrgsuppOLD  17811  psrbagaddcl  17891  psrbagaddclOLD  17892  gsumbagdiaglem  17898  psrass1lem  17900  psrlinv  17921  psrass1  17931  psrcom  17935  mplsubrglem  17971  mplsubrglemOLD  17972  mplmonmul  17997  mplcoe1  17998  mplcoe5  18002  mplcoe2OLD  18004  evlslem2  18051  evlslem6  18052  evlslem6OLD  18053  evlslem1  18055  coe1fval3  18118  coe1sclmul  18194  coe1sclmul2  18196  ply1coeOLD  18209  mulgrhm2  18403  mulgrhm2OLD  18406  cygznlem2a  18476  frgpcyg  18482  uvcresum  18694  frlmup1  18702  grpvrinv  18768  mhmvlin  18769  mdetleib2  18960  mdetralt  18980  mdetunilem9  18992  cayleyhamilton1  19263  neiptopnei  19503  dfac14  19989  ptcnp  19993  lmcn2  20020  cnmpt11f  20035  cnmpt21f  20043  cnmpt2k  20059  qtopeu  20087  xkocnv  20185  xkohmeo  20186  flfcnp2  20378  istgp2  20460  tmdgsum  20464  symgtgp  20470  subgtgp  20474  tgpconcomp  20481  prdstgpd  20493  tsmsmhm  20518  tsmssub  20521  tgptsmscls  20522  tsmssplit  20524  tsmsxplem1  20525  tlmtgp  20568  ustuqtop  20619  prdsmslem1  20900  prdsxmslem1  20901  prdsxmslem2  20902  tngnm  21035  nmoeq0  21113  cnfldnm  21156  cncfmpt1f  21287  negfcncf  21293  cnrehmeo  21323  evth  21329  evth2  21330  copco  21388  pcopt  21392  pcopt2  21393  pcoass  21394  pcorev2  21398  pi1xfrcnv  21427  ovolctb  21771  ovolfs2  21850  uniioombllem2  21862  uniioombllem3  21864  ismbf  21907  mbfconst  21912  ismbfcn2  21916  mbfmulc2re  21925  mbfadd  21938  mbfsub  21939  mbflimsup  21943  itg1climres  21991  mbfi1flimlem  21999  mbfi1flim  22000  mbfmul  22003  itg2uba  22020  itg2mulclem  22023  itg2mulc  22024  itg2splitlem  22025  itg2monolem1  22027  itg2i1fseq  22032  itg2gt0  22037  itg2cnlem1  22038  itg2cnlem2  22039  i1fibl  22084  itgitg1  22085  iblabslem  22104  iblabs  22105  bddmulibl  22115  cnplimc  22161  limccnp  22165  limccnp2  22166  dvcnp2  22193  dvmulf  22216  dvcmulf  22218  dvcobr  22219  dvcof  22221  dvcjbr  22222  dvcj  22223  dvfre  22224  dvmptcj  22241  dvcnvlem  22247  dvcnv  22248  dvef  22251  dvsincos  22252  rolle  22261  cmvth  22262  dvlip  22264  dvlipcn  22265  dv11cn  22272  dvivthlem1  22279  dvivth  22281  lhop2  22286  dvfsumrlim2  22303  ftc1lem1  22306  ftc1lem2  22307  ftc1a  22308  ftc1lem4  22310  ftc2  22315  ftc2ditglem  22316  ftc2ditg  22317  tdeglem4  22328  tdeglem2  22329  mdegle0  22347  mdegmullem  22348  plypf1  22479  plyco  22508  dgrcolem1  22539  dgrcolem2  22540  dgrco  22541  plycjlem  22542  dvply2g  22550  plydiveu  22563  elqaalem3  22586  taylthlem1  22637  taylthlem2  22638  ulmshft  22654  ulmdvlem1  22664  mtest  22668  mtestbdd  22669  mbfulm  22670  iblulm  22671  itgulm  22672  pserulm  22686  pserdv  22693  abelthlem1  22695  abelthlem3  22697  pige3  22779  eff1olem  22804  logcn  22897  advlog  22904  advlogexp  22905  logtayl  22910  logccv  22913  dvcxp1  22985  dvcxp2  22986  resqrtcn  22992  sqrtcn  22993  loglesqrt  23001  dvatan  23135  leibpi  23142  divsqrtsumo1  23182  jensenlem2  23186  amgmlem  23188  ftalem7  23221  basellem9  23231  muinv  23338  dchrmulid2  23396  dchrinvcl  23397  lgseisenlem4  23496  dchrisum0lem2a  23571  logdivsum  23587  mulog2sumlem1  23588  log2sumbnd  23598  hilnormi  25949  chscllem4  26427  hmopidmchi  26939  rabfodom  27273  cofmpt  27373  ofoprabco  27374  fpwrelmapffslem  27424  fpwrelmap  27425  qqhre  27868  esumpcvgval  27954  ofcfval4  27974  plymulx0  28374  lgamgulmlem2  28442  lgamcvg2  28467  ptpcon  28548  cvmliftlem6  28605  cvmliftlem8  28607  cvmlift2lem7  28624  cvmliftphtlem  28632  cvmlift3lem5  28638  elmsubrn  28758  mblfinlem2  30024  volsupnfl  30031  cnambfre  30035  dvtan  30037  itg2addnclem  30038  itg2addnclem2  30039  itg2addnclem3  30040  itg2addnc  30041  itg2gt0cn  30042  itgaddnc  30047  itgmulc2nc  30055  bddiblnc  30057  ftc1cnnclem  30060  ftc1anclem1  30062  ftc1anclem2  30063  ftc1anclem3  30064  ftc1anclem4  30065  ftc1anclem5  30066  ftc1anclem6  30067  ftc1anclem7  30068  ftc1anclem8  30069  ftc1anc  30070  ftc2nc  30071  dvcncxp1  30072  upixp  30192  mzpsubst  30653  diophun  30679  mendlmod  31115  mendassa  31116  cncfmptss  31509  mulcncff  31577  subcncff  31589  cncfcompt  31592  addcncff  31594  divcncff  31601  cncfiooicclem1  31603  dvsinexp  31609  dvsubf  31613  dvdivf  31623  dvcosax  31627  itgsinexplem1  31642  itgsubsticclem  31664  iblcncfioo  31667  itgiccshift  31669  stoweidlem20  31691  dirkercncflem2  31775  fourierdlem16  31794  fourierdlem21  31799  fourierdlem22  31800  fourierdlem28  31806  fourierdlem39  31817  fourierdlem51  31829  fourierdlem60  31838  fourierdlem61  31839  fourierdlem69  31847  fourierdlem72  31850  fourierdlem73  31851  fourierdlem81  31859  fourierdlem83  31861  fourierdlem84  31862  fourierdlem87  31865  fourierdlem90  31868  fourierdlem93  31871  fourierdlem95  31873  fourierdlem101  31879  fourierdlem103  31881  fourierdlem104  31882  fourierdlem111  31889
  Copyright terms: Public domain W3C validator