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

Theorem feqmptd 5843
Description: Deduction form of dffn5 5836. (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 5657 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
31, 2syl 16 . 2  |-  ( ph  ->  F  Fn  A )
4 dffn5 5836 . 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 1370    |-> cmpt 4448    Fn wfn 5511   -->wf 5512   ` cfv 5516
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pr 4629
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-sbc 3285  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-opab 4449  df-mpt 4450  df-id 4734  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-iota 5479  df-fun 5518  df-fn 5519  df-f 5520  df-fv 5524
This theorem is referenced by:  feqresmpt  5844  fcoconst  5979  suppssof1OLD  6439  ofco  6440  caofinvl  6447  caofcom  6452  caofass  6454  caofdi  6456  caofdir  6457  caonncan  6458  suppssof1  6822  mapxpen  7577  xpmapenlem  7578  cantnfp1  7990  cantnflem1  7998  cantnfp1OLD  8016  cantnflem1OLD  8021  cnfcom2lem  8035  cnfcom2lemOLD  8043  infxpenc  8285  infxpencOLD  8290  pwfseqlem5  8931  gruf  9079  ccatco  12565  cnrecnv  12756  lo1o12  13113  rlimclim1  13125  rlimuni  13130  lo1resb  13144  rlimresb  13145  o1resb  13146  rlimcn1  13168  rlimcn1b  13169  rlimo1  13196  o1rlimmul  13198  caucvgr  13255  ackbijnn  13393  bitsf1ocnv  13742  ramcl  14192  pwsplusgval  14530  pwsmulrval  14531  pwsvscafval  14534  setcepi  15058  prf1st  15116  prf2nd  15117  1st2ndprf  15118  curfuncf  15150  curf2ndf  15159  yonedainv  15193  yonffthlem  15194  prdsidlem  15555  pwsco1mhm  15600  pwsco2mhm  15601  frmdup3  15646  grpinvcnv  15696  pwsinvg  15769  pwssub  15770  psgnunilem5  16102  efginvrel1  16329  frgpup3lem  16378  frgpup3  16379  gsumval3OLD  16486  gsumval3  16489  gsumcllem  16490  gsumcllemOLD  16491  gsumzf1o  16495  gsumzf1oOLD  16498  gsumzsplit  16522  gsumzsplitOLD  16523  gsumconst  16532  gsumzmhm  16535  gsumzmhmOLD  16536  gsumsub  16552  gsumsubOLD  16553  gsum2dlem2  16567  gsum2dOLD  16569  gsumcom2  16572  dprdfadd  16615  dprdfsub  16616  dprdfeq0  16617  dprdf11  16618  dprdfaddOLD  16622  dprdfsubOLD  16623  dprdfeq0OLD  16624  dprdf11OLD  16625  dmdprdsplitlem  16639  dmdprdsplitlemOLD  16640  dprddisj2  16642  dprddisj2OLD  16643  dpjidcl  16662  dpjidclOLD  16669  ablfaclem2  16692  ablfac2  16695  lmhmvsca  17232  rrgsupp  17468  rrgsuppOLD  17469  psrbagaddcl  17544  psrbagaddclOLD  17545  gsumbagdiaglem  17551  psrass1lem  17553  psrlinv  17574  psrass1  17584  psrcom  17588  mplsubrglem  17624  mplsubrglemOLD  17625  mplmonmul  17650  mplcoe1  17651  mplcoe5  17655  mplcoe2OLD  17657  evlslem2  17704  evlslem6  17705  evlslem6OLD  17706  evlslem1  17708  coe1fval3  17771  coe1sclmul  17843  coe1sclmul2  17845  ply1coeOLD  17856  mulgrhm2  18036  mulgrhm2OLD  18039  cygznlem2a  18109  frgpcyg  18115  uvcresum  18327  frlmup1  18335  grpvrinv  18405  mhmvlin  18406  mdetleib2  18510  mdetralt  18530  mdetunilem9  18542  neiptopnei  18852  dfac14  19307  ptcnp  19311  lmcn2  19338  cnmpt11f  19353  cnmpt21f  19361  cnmpt2k  19377  qtopeu  19405  xkocnv  19503  xkohmeo  19504  flfcnp2  19696  istgp2  19778  tmdgsum  19782  symgtgp  19788  subgtgp  19792  tgpconcomp  19799  prdstgpd  19811  tsmsmhm  19836  tsmssub  19839  tgptsmscls  19840  tsmssplit  19842  tsmsxplem1  19843  tlmtgp  19886  ustuqtop  19937  prdsmslem1  20218  prdsxmslem1  20219  prdsxmslem2  20220  tngnm  20353  nmoeq0  20431  cnfldnm  20474  cncfmpt1f  20605  negfcncf  20611  cnrehmeo  20641  evth  20647  evth2  20648  copco  20706  pcopt  20710  pcopt2  20711  pcoass  20712  pcorev2  20716  pi1xfrcnv  20745  ovolctb  21089  ovolfs2  21167  uniioombllem2  21179  uniioombllem3  21181  ismbf  21224  mbfconst  21229  ismbfcn2  21233  mbfmulc2re  21242  mbfadd  21255  mbfsub  21256  mbflimsup  21260  itg1climres  21308  mbfi1flimlem  21316  mbfi1flim  21317  mbfmul  21320  itg2uba  21337  itg2mulclem  21340  itg2mulc  21341  itg2splitlem  21342  itg2monolem1  21344  itg2i1fseq  21349  itg2gt0  21354  itg2cnlem1  21355  itg2cnlem2  21356  i1fibl  21401  itgitg1  21402  iblabslem  21421  iblabs  21422  bddmulibl  21432  cnplimc  21478  limccnp  21482  limccnp2  21483  dvcnp2  21510  dvmulf  21533  dvcmulf  21535  dvcobr  21536  dvcof  21538  dvcjbr  21539  dvcj  21540  dvfre  21541  dvmptcj  21558  dvcnvlem  21564  dvcnv  21565  dvef  21568  dvsincos  21569  rolle  21578  cmvth  21579  dvlip  21581  dvlipcn  21582  dv11cn  21589  dvivthlem1  21596  dvivth  21598  lhop2  21603  dvfsumrlim2  21620  ftc1lem1  21623  ftc1lem2  21624  ftc1a  21625  ftc1lem4  21627  ftc2  21632  ftc2ditglem  21633  ftc2ditg  21634  tdeglem4  21645  tdeglem2  21646  mdegle0  21664  mdegmullem  21665  plypf1  21796  plyco  21825  dgrcolem1  21856  dgrcolem2  21857  dgrco  21858  plycjlem  21859  dvply2g  21867  plydiveu  21880  elqaalem3  21903  taylthlem1  21954  taylthlem2  21955  ulmshft  21971  ulmdvlem1  21981  mtest  21985  mtestbdd  21986  mbfulm  21987  iblulm  21988  itgulm  21989  pserulm  22003  pserdv  22010  abelthlem1  22012  abelthlem3  22014  pige3  22095  eff1olem  22120  logcn  22208  advlog  22215  advlogexp  22216  logtayl  22221  logccv  22224  dvcxp1  22296  dvcxp2  22297  resqrcn  22303  sqrcn  22304  loglesqr  22312  dvatan  22446  leibpi  22453  divsqrsumo1  22493  jensenlem2  22497  amgmlem  22499  ftalem7  22532  basellem9  22542  muinv  22649  dchrmulid2  22707  dchrinvcl  22708  lgseisenlem4  22807  dchrisum0lem2a  22882  logdivsum  22898  mulog2sumlem1  22899  log2sumbnd  22909  hilnormi  24700  chscllem4  25178  hmopidmchi  25690  cofmpt  26115  ofoprabco  26116  fpwrelmapffslem  26166  fpwrelmap  26167  qqhre  26580  esumpcvgval  26661  ofcfval4  26681  lgamgulmlem2  27150  lgamcvg2  27175  ptpcon  27256  cvmliftlem6  27313  cvmliftlem8  27315  cvmlift2lem7  27332  cvmliftphtlem  27340  cvmlift3lem5  27346  mblfinlem2  28567  volsupnfl  28574  cnambfre  28578  dvtan  28580  itg2addnclem  28581  itg2addnclem2  28582  itg2addnclem3  28583  itg2addnc  28584  itg2gt0cn  28585  itgaddnc  28590  itgmulc2nc  28598  bddiblnc  28600  ftc1cnnclem  28603  ftc1anclem1  28605  ftc1anclem2  28606  ftc1anclem3  28607  ftc1anclem4  28608  ftc1anclem5  28609  ftc1anclem6  28610  ftc1anclem7  28611  ftc1anclem8  28612  ftc1anc  28613  ftc2nc  28614  dvcncxp1  28615  upixp  28761  mzpsubst  29223  diophun  29250  mendlmod  29688  mendassa  29689  cncfmptss  29906  dvsinexp  29925  itgsinexplem1  29932  stoweidlem20  29953  cayleyhamilton1  31347
  Copyright terms: Public domain W3C validator