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

Theorem feqmptd 5925
Description: Deduction form of dffn5 5917. (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 5737 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
31, 2syl 17 . 2  |-  ( ph  ->  F  Fn  A )
4 dffn5 5917 . 2  |-  ( F  Fn  A  <->  F  =  ( x  e.  A  |->  ( F `  x
) ) )
53, 4sylib 199 1  |-  ( ph  ->  F  =  ( x  e.  A  |->  ( F `
 x ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    |-> cmpt 4475    Fn wfn 5587   -->wf 5588   ` cfv 5592
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pr 4652
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-rab 2782  df-v 3080  df-sbc 3297  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-br 4418  df-opab 4476  df-mpt 4477  df-id 4760  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-iota 5556  df-fun 5594  df-fn 5595  df-f 5596  df-fv 5600
This theorem is referenced by:  feqresmpt  5926  fcoconst  6066  ofco  6556  caofinvl  6563  caofcom  6568  caofass  6570  caofdi  6572  caofdir  6573  caonncan  6574  suppssof1  6950  mapxpen  7735  xpmapenlem  7736  cantnfp1  8176  cantnflem1  8184  cnfcom2lem  8196  infxpenc  8438  pwfseqlem5  9077  gruf  9225  ccatco  12906  cnrecnv  13196  lo1o12  13564  rlimclim1  13576  rlimuni  13581  lo1resb  13595  rlimresb  13596  o1resb  13597  rlimcn1  13619  rlimcn1b  13620  rlimo1  13647  o1rlimmul  13649  caucvgr  13708  ackbijnn  13853  bitsf1ocnv  14381  ramcl  14939  pwsplusgval  15340  pwsmulrval  15341  pwsvscafval  15344  setcepi  15927  prf1st  16033  prf2nd  16034  1st2ndprf  16035  curfuncf  16067  curf2ndf  16076  yonedainv  16110  yonffthlem  16111  prdsidlem  16512  pwsco1mhm  16561  pwsco2mhm  16562  frmdup3lem  16594  frmdup3  16595  grpinvcnv  16666  pwsinvg  16742  pwssub  16743  psgnunilem5  17079  efginvrel1  17306  frgpup3lem  17355  frgpup3  17356  gsumval3  17469  gsumcllem  17470  gsumzf1o  17474  gsumzsplit  17488  gsumconst  17495  gsumzmhm  17498  gsumsub  17509  gsum2dlem2  17531  gsumcom2  17535  dprdfadd  17581  dprdfsub  17582  dprdfeq0  17583  dprdf11  17584  dmdprdsplitlem  17598  dprddisj2  17600  dpjidcl  17619  ablfaclem2  17647  ablfac2  17650  mptscmfsuppd  18082  lmhmvsca  18196  rrgsupp  18443  psrbagaddcl  18522  gsumbagdiaglem  18527  psrass1lem  18529  psrlinv  18549  psrass1  18557  psrcom  18561  mplsubrglem  18591  mplmonmul  18616  mplcoe1  18617  mplcoe5  18620  evlslem2  18663  evlslem6  18664  evlslem1  18666  coe1fval3  18729  coe1sclmul  18803  coe1sclmul2  18805  ply1coeOLD  18818  mulgrhm2  18994  cygznlem2a  19062  frgpcyg  19068  uvcresum  19275  frlmup1  19280  grpvrinv  19345  mhmvlin  19346  mdetleib2  19537  mdetralt  19557  mdetunilem9  19569  cayleyhamilton1  19840  neiptopnei  20072  dfac14  20557  ptcnp  20561  lmcn2  20588  cnmpt11f  20603  cnmpt21f  20611  cnmpt2k  20627  qtopeu  20655  xkocnv  20753  xkohmeo  20754  flfcnp2  20946  istgp2  21030  tmdgsum  21034  symgtgp  21040  subgtgp  21044  tgpconcomp  21051  prdstgpd  21063  tsmsmhm  21084  tsmssub  21087  tgptsmscls  21088  tsmssplit  21090  tsmsxplem1  21091  tlmtgp  21134  ustuqtop  21185  prdsmslem1  21466  prdsxmslem1  21467  prdsxmslem2  21468  tngnm  21583  nmoeq0  21661  cnfldnm  21703  cncfmpt1f  21834  negfcncf  21840  cnrehmeo  21870  evth  21876  evth2  21877  copco  21935  pcopt  21939  pcopt2  21940  pcoass  21941  pcorev2  21945  pi1xfrcnv  21974  ovolctb  22317  ovolfs2  22397  uniioombllem2  22414  uniioombllem2OLD  22415  uniioombllem3  22417  ismbf  22460  mbfconst  22465  ismbfcn2  22469  mbfmulc2re  22478  mbfadd  22491  mbfsub  22492  mbflimsup  22497  mbflimsupOLD  22498  itg1climres  22546  mbfi1flimlem  22554  mbfi1flim  22555  mbfmul  22558  itg2uba  22575  itg2mulclem  22578  itg2mulc  22579  itg2splitlem  22580  itg2monolem1  22582  itg2i1fseq  22587  itg2gt0  22592  itg2cnlem1  22593  itg2cnlem2  22594  i1fibl  22639  itgitg1  22640  iblabslem  22659  iblabs  22660  bddmulibl  22670  cnplimc  22716  limccnp  22720  limccnp2  22721  dvcnp2  22748  dvmulf  22771  dvcmulf  22773  dvcobr  22774  dvcof  22776  dvcjbr  22777  dvcj  22778  dvfre  22779  dvmptcj  22796  dvcnvlem  22802  dvcnv  22803  dvef  22806  dvsincos  22807  rolle  22816  cmvth  22817  dvlip  22819  dvlipcn  22820  dv11cn  22827  dvivthlem1  22834  dvivth  22836  lhop2  22841  dvfsumrlim2  22858  ftc1lem1  22861  ftc1lem2  22862  ftc1a  22863  ftc1lem4  22865  ftc2  22870  ftc2ditglem  22871  ftc2ditg  22872  tdeglem4  22883  tdeglem2  22884  mdegle0  22900  mdegmullem  22901  plypf1  23031  plyco  23060  dgrcolem1  23092  dgrcolem2  23093  dgrco  23094  plycjlem  23095  dvply2g  23103  plydiveu  23116  elqaalem3  23139  taylthlem1  23190  taylthlem2  23191  ulmshft  23207  ulmdvlem1  23217  mtest  23221  mtestbdd  23222  mbfulm  23223  iblulm  23224  itgulm  23225  pserulm  23239  pserdv  23246  abelthlem1  23248  abelthlem3  23250  pige3  23334  eff1olem  23359  logcn  23454  advlog  23461  advlogexp  23462  logtayl  23467  logccv  23470  dvcxp1  23542  dvcxp2  23543  dvcncxp1  23545  resqrtcn  23551  sqrtcn  23552  loglesqrt  23560  dvatan  23723  leibpi  23730  divsqrtsumo1  23771  jensenlem2  23775  amgmlem  23777  lgamgulmlem2  23817  lgamcvg2  23842  ftalem7  23865  basellem9  23875  muinv  23982  dchrmulid2  24040  dchrinvcl  24041  lgseisenlem4  24140  dchrisum0lem2a  24215  logdivsum  24231  mulog2sumlem1  24232  log2sumbnd  24242  hilnormi  26648  chscllem4  27125  hmopidmchi  27636  rabfodom  27973  cofmpt  28103  ofoprabco  28104  fpwrelmapffslem  28157  fpwrelmap  28158  qqhre  28660  esumpcvgval  28735  ofcfval4  28762  omssubadd  28958  carsggect  28976  plymulx0  29221  ptpcon  29741  cvmliftlem6  29798  cvmliftlem8  29800  cvmlift2lem7  29817  cvmliftphtlem  29825  cvmlift3lem5  29831  elmsubrn  29951  poimir  31677  broucube  31678  mblfinlem2  31682  volsupnfl  31689  cnambfre  31693  dvtan  31696  itg2addnclem  31697  itg2addnclem2  31698  itg2addnclem3  31699  itg2addnc  31700  itg2gt0cn  31701  itgaddnc  31706  itgmulc2nc  31714  bddiblnc  31716  ftc1cnnclem  31719  ftc1anclem1  31721  ftc1anclem2  31722  ftc1anclem3  31723  ftc1anclem4  31724  ftc1anclem5  31725  ftc1anclem6  31726  ftc1anclem7  31727  ftc1anclem8  31728  ftc1anc  31729  ftc2nc  31730  upixp  31760  mzpsubst  35299  diophun  35325  mendlmod  35762  mendassa  35763  binomcxplemnotnn0  36346  rnsnf  37085  cncfmptss  37241  mulcncff  37321  subcncff  37333  cncfcompt  37336  addcncff  37338  divcncff  37345  cncfiooicclem1  37347  dvsinexp  37356  dvsubf  37360  dvdivf  37370  dvcosax  37374  dvnmul  37391  dvnprodlem1  37394  dvnprodlem2  37395  itgsinexplem1  37403  itgsubsticclem  37425  iblcncfioo  37428  itgiccshift  37430  stoweidlem20  37453  dirkercncflem2  37539  fourierdlem16  37558  fourierdlem21  37563  fourierdlem22  37564  fourierdlem28  37570  fourierdlem39  37581  fourierdlem51  37593  fourierdlem60  37602  fourierdlem61  37603  fourierdlem69  37611  fourierdlem72  37614  fourierdlem73  37615  fourierdlem81  37623  fourierdlem83  37625  fourierdlem84  37626  fourierdlem87  37629  fourierdlem90  37632  fourierdlem93  37635  fourierdlem95  37637  fourierdlem101  37643  fourierdlem103  37645  fourierdlem104  37646  fourierdlem111  37653  etransclem34  37704  etransclem43  37713  etransclem46  37716  sge0tsms  37760  sge0fodjrnlem  37796  sge0iun  37799  meadjun  37813  meadjiunlem  37816  meadjiun  37817  ismeannd  37818  psmeasurelem  37821  omeiunle  37851  aacllem  39314
  Copyright terms: Public domain W3C validator