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

Theorem feqmptd 5918
Description: Deduction form of dffn5 5911. (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 5729 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
31, 2syl 16 . 2  |-  ( ph  ->  F  Fn  A )
4 dffn5 5911 . 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 1379    |-> cmpt 4505    Fn wfn 5581   -->wf 5582   ` cfv 5586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-fv 5594
This theorem is referenced by:  feqresmpt  5919  fcoconst  6056  suppssof1OLD  6541  ofco  6542  caofinvl  6549  caofcom  6554  caofass  6556  caofdi  6558  caofdir  6559  caonncan  6560  suppssof1  6930  mapxpen  7680  xpmapenlem  7681  cantnfp1  8096  cantnflem1  8104  cantnfp1OLD  8122  cantnflem1OLD  8127  cnfcom2lem  8141  cnfcom2lemOLD  8149  infxpenc  8391  infxpencOLD  8396  pwfseqlem5  9037  gruf  9185  ccatco  12760  cnrecnv  12957  lo1o12  13315  rlimclim1  13327  rlimuni  13332  lo1resb  13346  rlimresb  13347  o1resb  13348  rlimcn1  13370  rlimcn1b  13371  rlimo1  13398  o1rlimmul  13400  caucvgr  13457  ackbijnn  13599  bitsf1ocnv  13949  ramcl  14402  pwsplusgval  14741  pwsmulrval  14742  pwsvscafval  14745  setcepi  15269  prf1st  15327  prf2nd  15328  1st2ndprf  15329  curfuncf  15361  curf2ndf  15370  yonedainv  15404  yonffthlem  15405  prdsidlem  15766  pwsco1mhm  15811  pwsco2mhm  15812  frmdup3  15857  grpinvcnv  15907  pwsinvg  15982  pwssub  15983  psgnunilem5  16315  efginvrel1  16542  frgpup3lem  16591  frgpup3  16592  gsumval3OLD  16699  gsumval3  16702  gsumcllem  16703  gsumcllemOLD  16704  gsumzf1o  16708  gsumzf1oOLD  16711  gsumzsplit  16735  gsumzsplitOLD  16736  gsumconst  16745  gsumzmhm  16748  gsumzmhmOLD  16749  gsumsub  16765  gsumsubOLD  16766  gsum2dlem2  16789  gsum2dOLD  16791  gsumcom2  16794  dprdfadd  16850  dprdfsub  16851  dprdfeq0  16852  dprdf11  16853  dprdfaddOLD  16857  dprdfsubOLD  16858  dprdfeq0OLD  16859  dprdf11OLD  16860  dmdprdsplitlem  16874  dmdprdsplitlemOLD  16875  dprddisj2  16877  dprddisj2OLD  16878  dpjidcl  16897  dpjidclOLD  16904  ablfaclem2  16927  ablfac2  16930  lmhmvsca  17474  rrgsupp  17710  rrgsuppOLD  17711  psrbagaddcl  17791  psrbagaddclOLD  17792  gsumbagdiaglem  17798  psrass1lem  17800  psrlinv  17821  psrass1  17831  psrcom  17835  mplsubrglem  17871  mplsubrglemOLD  17872  mplmonmul  17897  mplcoe1  17898  mplcoe5  17902  mplcoe2OLD  17904  evlslem2  17951  evlslem6  17952  evlslem6OLD  17953  evlslem1  17955  coe1fval3  18018  coe1sclmul  18094  coe1sclmul2  18096  ply1coeOLD  18109  mulgrhm2  18300  mulgrhm2OLD  18303  cygznlem2a  18373  frgpcyg  18379  uvcresum  18591  frlmup1  18599  grpvrinv  18665  mhmvlin  18666  mdetleib2  18857  mdetralt  18877  mdetunilem9  18889  cayleyhamilton1  19160  neiptopnei  19399  dfac14  19854  ptcnp  19858  lmcn2  19885  cnmpt11f  19900  cnmpt21f  19908  cnmpt2k  19924  qtopeu  19952  xkocnv  20050  xkohmeo  20051  flfcnp2  20243  istgp2  20325  tmdgsum  20329  symgtgp  20335  subgtgp  20339  tgpconcomp  20346  prdstgpd  20358  tsmsmhm  20383  tsmssub  20386  tgptsmscls  20387  tsmssplit  20389  tsmsxplem1  20390  tlmtgp  20433  ustuqtop  20484  prdsmslem1  20765  prdsxmslem1  20766  prdsxmslem2  20767  tngnm  20900  nmoeq0  20978  cnfldnm  21021  cncfmpt1f  21152  negfcncf  21158  cnrehmeo  21188  evth  21194  evth2  21195  copco  21253  pcopt  21257  pcopt2  21258  pcoass  21259  pcorev2  21263  pi1xfrcnv  21292  ovolctb  21636  ovolfs2  21715  uniioombllem2  21727  uniioombllem3  21729  ismbf  21772  mbfconst  21777  ismbfcn2  21781  mbfmulc2re  21790  mbfadd  21803  mbfsub  21804  mbflimsup  21808  itg1climres  21856  mbfi1flimlem  21864  mbfi1flim  21865  mbfmul  21868  itg2uba  21885  itg2mulclem  21888  itg2mulc  21889  itg2splitlem  21890  itg2monolem1  21892  itg2i1fseq  21897  itg2gt0  21902  itg2cnlem1  21903  itg2cnlem2  21904  i1fibl  21949  itgitg1  21950  iblabslem  21969  iblabs  21970  bddmulibl  21980  cnplimc  22026  limccnp  22030  limccnp2  22031  dvcnp2  22058  dvmulf  22081  dvcmulf  22083  dvcobr  22084  dvcof  22086  dvcjbr  22087  dvcj  22088  dvfre  22089  dvmptcj  22106  dvcnvlem  22112  dvcnv  22113  dvef  22116  dvsincos  22117  rolle  22126  cmvth  22127  dvlip  22129  dvlipcn  22130  dv11cn  22137  dvivthlem1  22144  dvivth  22146  lhop2  22151  dvfsumrlim2  22168  ftc1lem1  22171  ftc1lem2  22172  ftc1a  22173  ftc1lem4  22175  ftc2  22180  ftc2ditglem  22181  ftc2ditg  22182  tdeglem4  22193  tdeglem2  22194  mdegle0  22212  mdegmullem  22213  plypf1  22344  plyco  22373  dgrcolem1  22404  dgrcolem2  22405  dgrco  22406  plycjlem  22407  dvply2g  22415  plydiveu  22428  elqaalem3  22451  taylthlem1  22502  taylthlem2  22503  ulmshft  22519  ulmdvlem1  22529  mtest  22533  mtestbdd  22534  mbfulm  22535  iblulm  22536  itgulm  22537  pserulm  22551  pserdv  22558  abelthlem1  22560  abelthlem3  22562  pige3  22643  eff1olem  22668  logcn  22756  advlog  22763  advlogexp  22764  logtayl  22769  logccv  22772  dvcxp1  22844  dvcxp2  22845  resqrtcn  22851  sqrtcn  22852  loglesqrt  22860  dvatan  22994  leibpi  23001  divsqrtsumo1  23041  jensenlem2  23045  amgmlem  23047  ftalem7  23080  basellem9  23090  muinv  23197  dchrmulid2  23255  dchrinvcl  23256  lgseisenlem4  23355  dchrisum0lem2a  23430  logdivsum  23446  mulog2sumlem1  23447  log2sumbnd  23457  hilnormi  25756  chscllem4  26234  hmopidmchi  26746  cofmpt  27176  ofoprabco  27177  fpwrelmapffslem  27227  fpwrelmap  27228  qqhre  27634  esumpcvgval  27724  ofcfval4  27744  lgamgulmlem2  28212  lgamcvg2  28237  ptpcon  28318  cvmliftlem6  28375  cvmliftlem8  28377  cvmlift2lem7  28394  cvmliftphtlem  28402  cvmlift3lem5  28408  mblfinlem2  29629  volsupnfl  29636  cnambfre  29640  dvtan  29642  itg2addnclem  29643  itg2addnclem2  29644  itg2addnclem3  29645  itg2addnc  29646  itg2gt0cn  29647  itgaddnc  29652  itgmulc2nc  29660  bddiblnc  29662  ftc1cnnclem  29665  ftc1anclem1  29667  ftc1anclem2  29668  ftc1anclem3  29669  ftc1anclem4  29670  ftc1anclem5  29671  ftc1anclem6  29672  ftc1anclem7  29673  ftc1anclem8  29674  ftc1anc  29675  ftc2nc  29676  dvcncxp1  29677  upixp  29823  mzpsubst  30285  diophun  30311  mendlmod  30747  mendassa  30748  cncfmptss  31137  mulcncff  31206  subcncff  31218  cncfcompt  31221  addcncff  31223  divcncff  31230  cncfiooicclem1  31232  dvsinexp  31238  dvsubf  31242  dvdivf  31252  dvcosax  31256  itgsinexplem1  31271  iblcncfioo  31296  itgiccshift  31298  stoweidlem20  31320  fourierdlem16  31423  fourierdlem21  31428  fourierdlem22  31429  fourierdlem23  31430  fourierdlem28  31435  fourierdlem39  31446  fourierdlem51  31458  fourierdlem60  31467  fourierdlem61  31468  fourierdlem69  31476  fourierdlem72  31479  fourierdlem73  31480  fourierdlem81  31488  fourierdlem83  31490  fourierdlem84  31491  fourierdlem87  31494  fourierdlem93  31500  fourierdlem95  31502  fourierdlem101  31508  fourierdlem103  31510  fourierdlem104  31511  fourierdlem111  31518
  Copyright terms: Public domain W3C validator