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

Theorem feqmptd 5732
Description: Deduction form of dffn5 5725. (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 5547 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
31, 2syl 16 . 2  |-  ( ph  ->  F  Fn  A )
4 dffn5 5725 . 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 1362    e. cmpt 4338    Fn wfn 5401   -->wf 5402   ` cfv 5406
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-fv 5414
This theorem is referenced by:  feqresmpt  5733  fcoconst  5867  suppssof1OLD  6328  ofco  6329  caofinvl  6336  caofcom  6341  caofass  6343  caofdi  6345  caofdir  6346  caonncan  6347  suppssof1  6711  mapxpen  7465  xpmapenlem  7466  cantnfp1  7877  cantnflem1  7885  cantnfp1OLD  7903  cantnflem1OLD  7908  cnfcom2lem  7922  cnfcom2lemOLD  7930  infxpenc  8172  infxpencOLD  8177  pwfseqlem5  8817  gruf  8965  ccatco  12446  cnrecnv  12637  lo1o12  12994  rlimclim1  13006  rlimuni  13011  lo1resb  13025  rlimresb  13026  o1resb  13027  rlimcn1  13049  rlimcn1b  13050  rlimo1  13077  o1rlimmul  13079  caucvgr  13136  ackbijnn  13273  bitsf1ocnv  13622  ramcl  14072  pwsplusgval  14410  pwsmulrval  14411  pwsvscafval  14414  setcepi  14938  prf1st  14996  prf2nd  14997  1st2ndprf  14998  curfuncf  15030  curf2ndf  15039  yonedainv  15073  yonffthlem  15074  prdsidlem  15435  pwsco1mhm  15479  pwsco2mhm  15480  frmdup3  15523  grpinvcnv  15573  pwsinvg  15646  pwssub  15647  psgnunilem5  15979  efginvrel1  16204  frgpup3lem  16253  frgpup3  16254  gsumval3OLD  16361  gsumval3  16364  gsumcllem  16365  gsumcllemOLD  16366  gsumzf1o  16370  gsumzf1oOLD  16373  gsumzsplit  16397  gsumzsplitOLD  16398  gsumconst  16405  gsumzmhm  16406  gsumzmhmOLD  16407  gsumsub  16422  gsumsubOLD  16423  gsum2dlem2  16435  gsum2dOLD  16437  gsumcom2  16440  dprdfadd  16483  dprdfsub  16484  dprdfeq0  16485  dprdf11  16486  dprdfaddOLD  16490  dprdfsubOLD  16491  dprdfeq0OLD  16492  dprdf11OLD  16493  dmdprdsplitlem  16507  dmdprdsplitlemOLD  16508  dprddisj2  16510  dprddisj2OLD  16511  dpjidcl  16530  dpjidclOLD  16537  ablfaclem2  16560  ablfac2  16563  lmhmvsca  17047  rrgsupp  17283  rrgsuppOLD  17284  psrbagaddcl  17371  psrbagaddclOLD  17372  gsumbagdiaglem  17378  psrass1lem  17380  psrlinv  17401  psrass1  17411  psrcom  17414  mplsubrglem  17450  mplsubrglemOLD  17451  mplmonmul  17476  mplcoe1  17477  mplcoe2  17480  mplcoe2OLD  17481  evlslem2  17524  coe1fval3  17562  coe1sclmul  17632  coe1sclmul2  17634  ply1coe  17642  mulgrhm2  17768  mulgrhm2OLD  17771  cygznlem2a  17841  frgpcyg  17847  uvcresum  18059  frlmup1  18067  grpvrinv  18137  mhmvlin  18138  mdetleib2  18240  mdetralt  18255  mdetunilem9  18267  neiptopnei  18577  dfac14  19032  ptcnp  19036  lmcn2  19063  cnmpt11f  19078  cnmpt21f  19086  cnmpt2k  19102  qtopeu  19130  xkocnv  19228  xkohmeo  19229  flfcnp2  19421  istgp2  19503  tmdgsum  19507  symgtgp  19513  subgtgp  19517  tgpconcomp  19524  prdstgpd  19536  tsmsmhm  19561  tsmssub  19564  tgptsmscls  19565  tsmssplit  19567  tsmsxplem1  19568  tlmtgp  19611  ustuqtop  19662  prdsmslem1  19943  prdsxmslem1  19944  prdsxmslem2  19945  tngnm  20078  nmoeq0  20156  cnfldnm  20199  cncfmpt1f  20330  negfcncf  20336  cnrehmeo  20366  evth  20372  evth2  20373  copco  20431  pcopt  20435  pcopt2  20436  pcoass  20437  pcorev2  20441  pi1xfrcnv  20470  ovolctb  20814  ovolfs2  20892  uniioombllem2  20904  uniioombllem3  20906  ismbf  20949  mbfconst  20954  ismbfcn2  20958  mbfmulc2re  20967  mbfadd  20980  mbfsub  20981  mbflimsup  20985  itg1climres  21033  mbfi1flimlem  21041  mbfi1flim  21042  mbfmul  21045  itg2uba  21062  itg2mulclem  21065  itg2mulc  21066  itg2splitlem  21067  itg2monolem1  21069  itg2i1fseq  21074  itg2gt0  21079  itg2cnlem1  21080  itg2cnlem2  21081  i1fibl  21126  itgitg1  21127  iblabslem  21146  iblabs  21147  bddmulibl  21157  cnplimc  21203  limccnp  21207  limccnp2  21208  dvcnp2  21235  dvmulf  21258  dvcmulf  21260  dvcobr  21261  dvcof  21263  dvcjbr  21264  dvcj  21265  dvfre  21266  dvmptcj  21283  dvcnvlem  21289  dvcnv  21290  dvef  21293  dvsincos  21294  rolle  21303  cmvth  21304  dvlip  21306  dvlipcn  21307  dv11cn  21314  dvivthlem1  21321  dvivth  21323  lhop2  21328  dvfsumrlim2  21345  ftc1lem1  21348  ftc1lem2  21349  ftc1a  21350  ftc1lem4  21352  ftc2  21357  ftc2ditglem  21358  ftc2ditg  21359  evlslem6  21363  evlslem6OLD  21364  evlslem1  21366  tdeglem4  21413  tdeglem2  21414  mdegle0  21432  mdegmullem  21433  plypf1  21564  plyco  21593  dgrcolem1  21624  dgrcolem2  21625  dgrco  21626  plycjlem  21627  dvply2g  21635  plydiveu  21648  elqaalem3  21671  taylthlem1  21722  taylthlem2  21723  ulmshft  21739  ulmdvlem1  21749  mtest  21753  mtestbdd  21754  mbfulm  21755  iblulm  21756  itgulm  21757  pserulm  21771  pserdv  21778  abelthlem1  21780  abelthlem3  21782  pige3  21863  eff1olem  21888  logcn  21976  advlog  21983  advlogexp  21984  logtayl  21989  logccv  21992  dvcxp1  22064  dvcxp2  22065  resqrcn  22071  sqrcn  22072  loglesqr  22080  dvatan  22214  leibpi  22221  divsqrsumo1  22261  jensenlem2  22265  amgmlem  22267  ftalem7  22300  basellem9  22310  muinv  22417  dchrmulid2  22475  dchrinvcl  22476  lgseisenlem4  22575  dchrisum0lem2a  22650  logdivsum  22666  mulog2sumlem1  22667  log2sumbnd  22677  hilnormi  24387  chscllem4  24865  hmopidmchi  25377  cofmpt  25804  ofoprabco  25805  fpwrelmapffslem  25856  fpwrelmap  25857  qqhre  26299  esumpcvgval  26380  ofcfval4  26400  lgamgulmlem2  26863  lgamcvg2  26888  ptpcon  26969  cvmliftlem6  27026  cvmliftlem8  27028  cvmlift2lem7  27045  cvmliftphtlem  27053  cvmlift3lem5  27059  mblfinlem2  28270  volsupnfl  28277  cnambfre  28281  dvtan  28283  itg2addnclem  28284  itg2addnclem2  28285  itg2addnclem3  28286  itg2addnc  28287  itg2gt0cn  28288  itgaddnc  28293  itgmulc2nc  28301  bddiblnc  28303  ftc1cnnclem  28306  ftc1anclem1  28308  ftc1anclem2  28309  ftc1anclem3  28310  ftc1anclem4  28311  ftc1anclem5  28312  ftc1anclem6  28313  ftc1anclem7  28314  ftc1anclem8  28315  ftc1anc  28316  ftc2nc  28317  dvcncxp1  28318  upixp  28464  mzpsubst  28927  diophun  28954  mendlmod  29392  mendassa  29393  cncfmptss  29610  dvsinexp  29630  itgsinexplem1  29637  stoweidlem20  29658  mptscmfsuppd  30630  ply1coefsupp  30631
  Copyright terms: Public domain W3C validator