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

Theorem feqmptd 5739
Description: Deduction form of dffn5 5732. (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 5554 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
31, 2syl 16 . 2  |-  ( ph  ->  F  Fn  A )
4 dffn5 5732 . 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 1369    e. cmpt 4345    Fn wfn 5408   -->wf 5409   ` cfv 5413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-fv 5421
This theorem is referenced by:  feqresmpt  5740  fcoconst  5875  suppssof1OLD  6334  ofco  6335  caofinvl  6342  caofcom  6347  caofass  6349  caofdi  6351  caofdir  6352  caonncan  6353  suppssof1  6717  mapxpen  7469  xpmapenlem  7470  cantnfp1  7881  cantnflem1  7889  cantnfp1OLD  7907  cantnflem1OLD  7912  cnfcom2lem  7926  cnfcom2lemOLD  7934  infxpenc  8176  infxpencOLD  8181  pwfseqlem5  8822  gruf  8970  ccatco  12455  cnrecnv  12646  lo1o12  13003  rlimclim1  13015  rlimuni  13020  lo1resb  13034  rlimresb  13035  o1resb  13036  rlimcn1  13058  rlimcn1b  13059  rlimo1  13086  o1rlimmul  13088  caucvgr  13145  ackbijnn  13283  bitsf1ocnv  13632  ramcl  14082  pwsplusgval  14420  pwsmulrval  14421  pwsvscafval  14424  setcepi  14948  prf1st  15006  prf2nd  15007  1st2ndprf  15008  curfuncf  15040  curf2ndf  15049  yonedainv  15083  yonffthlem  15084  prdsidlem  15445  pwsco1mhm  15489  pwsco2mhm  15490  frmdup3  15535  grpinvcnv  15585  pwsinvg  15658  pwssub  15659  psgnunilem5  15991  efginvrel1  16216  frgpup3lem  16265  frgpup3  16266  gsumval3OLD  16373  gsumval3  16376  gsumcllem  16377  gsumcllemOLD  16378  gsumzf1o  16382  gsumzf1oOLD  16385  gsumzsplit  16409  gsumzsplitOLD  16410  gsumconst  16417  gsumzmhm  16420  gsumzmhmOLD  16421  gsumsub  16437  gsumsubOLD  16438  gsum2dlem2  16452  gsum2dOLD  16454  gsumcom2  16457  dprdfadd  16500  dprdfsub  16501  dprdfeq0  16502  dprdf11  16503  dprdfaddOLD  16507  dprdfsubOLD  16508  dprdfeq0OLD  16509  dprdf11OLD  16510  dmdprdsplitlem  16524  dmdprdsplitlemOLD  16525  dprddisj2  16527  dprddisj2OLD  16528  dpjidcl  16547  dpjidclOLD  16554  ablfaclem2  16577  ablfac2  16580  lmhmvsca  17106  rrgsupp  17342  rrgsuppOLD  17343  psrbagaddcl  17418  psrbagaddclOLD  17419  gsumbagdiaglem  17425  psrass1lem  17427  psrlinv  17448  psrass1  17458  psrcom  17461  mplsubrglem  17497  mplsubrglemOLD  17498  mplmonmul  17523  mplcoe1  17524  mplcoe5  17528  mplcoe2OLD  17530  evlslem2  17577  evlslem6  17578  evlslem6OLD  17579  evlslem1  17581  coe1fval3  17644  coe1sclmul  17715  coe1sclmul2  17717  ply1coeOLD  17727  mulgrhm2  17907  mulgrhm2OLD  17910  cygznlem2a  17980  frgpcyg  17986  uvcresum  18198  frlmup1  18206  grpvrinv  18276  mhmvlin  18277  mdetleib2  18379  mdetralt  18394  mdetunilem9  18406  neiptopnei  18716  dfac14  19171  ptcnp  19175  lmcn2  19202  cnmpt11f  19217  cnmpt21f  19225  cnmpt2k  19241  qtopeu  19269  xkocnv  19367  xkohmeo  19368  flfcnp2  19560  istgp2  19642  tmdgsum  19646  symgtgp  19652  subgtgp  19656  tgpconcomp  19663  prdstgpd  19675  tsmsmhm  19700  tsmssub  19703  tgptsmscls  19704  tsmssplit  19706  tsmsxplem1  19707  tlmtgp  19750  ustuqtop  19801  prdsmslem1  20082  prdsxmslem1  20083  prdsxmslem2  20084  tngnm  20217  nmoeq0  20295  cnfldnm  20338  cncfmpt1f  20469  negfcncf  20475  cnrehmeo  20505  evth  20511  evth2  20512  copco  20570  pcopt  20574  pcopt2  20575  pcoass  20576  pcorev2  20580  pi1xfrcnv  20609  ovolctb  20953  ovolfs2  21031  uniioombllem2  21043  uniioombllem3  21045  ismbf  21088  mbfconst  21093  ismbfcn2  21097  mbfmulc2re  21106  mbfadd  21119  mbfsub  21120  mbflimsup  21124  itg1climres  21172  mbfi1flimlem  21180  mbfi1flim  21181  mbfmul  21184  itg2uba  21201  itg2mulclem  21204  itg2mulc  21205  itg2splitlem  21206  itg2monolem1  21208  itg2i1fseq  21213  itg2gt0  21218  itg2cnlem1  21219  itg2cnlem2  21220  i1fibl  21265  itgitg1  21266  iblabslem  21285  iblabs  21286  bddmulibl  21296  cnplimc  21342  limccnp  21346  limccnp2  21347  dvcnp2  21374  dvmulf  21397  dvcmulf  21399  dvcobr  21400  dvcof  21402  dvcjbr  21403  dvcj  21404  dvfre  21405  dvmptcj  21422  dvcnvlem  21428  dvcnv  21429  dvef  21432  dvsincos  21433  rolle  21442  cmvth  21443  dvlip  21445  dvlipcn  21446  dv11cn  21453  dvivthlem1  21460  dvivth  21462  lhop2  21467  dvfsumrlim2  21484  ftc1lem1  21487  ftc1lem2  21488  ftc1a  21489  ftc1lem4  21491  ftc2  21496  ftc2ditglem  21497  ftc2ditg  21498  tdeglem4  21509  tdeglem2  21510  mdegle0  21528  mdegmullem  21529  plypf1  21660  plyco  21689  dgrcolem1  21720  dgrcolem2  21721  dgrco  21722  plycjlem  21723  dvply2g  21731  plydiveu  21744  elqaalem3  21767  taylthlem1  21818  taylthlem2  21819  ulmshft  21835  ulmdvlem1  21845  mtest  21849  mtestbdd  21850  mbfulm  21851  iblulm  21852  itgulm  21853  pserulm  21867  pserdv  21874  abelthlem1  21876  abelthlem3  21878  pige3  21959  eff1olem  21984  logcn  22072  advlog  22079  advlogexp  22080  logtayl  22085  logccv  22088  dvcxp1  22160  dvcxp2  22161  resqrcn  22167  sqrcn  22168  loglesqr  22176  dvatan  22310  leibpi  22317  divsqrsumo1  22357  jensenlem2  22361  amgmlem  22363  ftalem7  22396  basellem9  22406  muinv  22513  dchrmulid2  22571  dchrinvcl  22572  lgseisenlem4  22671  dchrisum0lem2a  22746  logdivsum  22762  mulog2sumlem1  22763  log2sumbnd  22773  hilnormi  24533  chscllem4  25011  hmopidmchi  25523  cofmpt  25949  ofoprabco  25950  fpwrelmapffslem  26000  fpwrelmap  26001  qqhre  26415  esumpcvgval  26496  ofcfval4  26516  lgamgulmlem2  26985  lgamcvg2  27010  ptpcon  27091  cvmliftlem6  27148  cvmliftlem8  27150  cvmlift2lem7  27167  cvmliftphtlem  27175  cvmlift3lem5  27181  mblfinlem2  28400  volsupnfl  28407  cnambfre  28411  dvtan  28413  itg2addnclem  28414  itg2addnclem2  28415  itg2addnclem3  28416  itg2addnc  28417  itg2gt0cn  28418  itgaddnc  28423  itgmulc2nc  28431  bddiblnc  28433  ftc1cnnclem  28436  ftc1anclem1  28438  ftc1anclem2  28439  ftc1anclem3  28440  ftc1anclem4  28441  ftc1anclem5  28442  ftc1anclem6  28443  ftc1anclem7  28444  ftc1anclem8  28445  ftc1anc  28446  ftc2nc  28447  dvcncxp1  28448  upixp  28594  mzpsubst  29056  diophun  29083  mendlmod  29521  mendassa  29522  cncfmptss  29739  dvsinexp  29758  itgsinexplem1  29765  stoweidlem20  29786
  Copyright terms: Public domain W3C validator