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

Theorem feqmptd 5901
Description: Deduction form of dffn5 5893. (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 5713 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
31, 2syl 16 . 2  |-  ( ph  ->  F  Fn  A )
4 dffn5 5893 . 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 1398    |-> cmpt 4497    Fn wfn 5565   -->wf 5566   ` cfv 5570
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-fv 5578
This theorem is referenced by:  feqresmpt  5902  fcoconst  6044  suppssof1OLD  6532  ofco  6533  caofinvl  6540  caofcom  6545  caofass  6547  caofdi  6549  caofdir  6550  caonncan  6551  suppssof1  6925  mapxpen  7676  xpmapenlem  7677  cantnfp1  8091  cantnflem1  8099  cantnfp1OLD  8117  cantnflem1OLD  8122  cnfcom2lem  8136  cnfcom2lemOLD  8144  infxpenc  8386  infxpencOLD  8391  pwfseqlem5  9030  gruf  9178  ccatco  12792  cnrecnv  13080  lo1o12  13438  rlimclim1  13450  rlimuni  13455  lo1resb  13469  rlimresb  13470  o1resb  13471  rlimcn1  13493  rlimcn1b  13494  rlimo1  13521  o1rlimmul  13523  caucvgr  13580  ackbijnn  13722  bitsf1ocnv  14178  ramcl  14631  pwsplusgval  14979  pwsmulrval  14980  pwsvscafval  14983  setcepi  15566  prf1st  15672  prf2nd  15673  1st2ndprf  15674  curfuncf  15706  curf2ndf  15715  yonedainv  15749  yonffthlem  15750  prdsidlem  16151  pwsco1mhm  16200  pwsco2mhm  16201  frmdup3lem  16233  frmdup3  16234  grpinvcnv  16305  pwsinvg  16381  pwssub  16382  psgnunilem5  16718  efginvrel1  16945  frgpup3lem  16994  frgpup3  16995  gsumval3OLD  17107  gsumval3  17110  gsumcllem  17111  gsumcllemOLD  17112  gsumzf1o  17116  gsumzf1oOLD  17119  gsumzsplit  17143  gsumzsplitOLD  17144  gsumconst  17152  gsumzmhm  17155  gsumzmhmOLD  17156  gsumsub  17171  gsum2dlem2  17194  gsum2dOLD  17196  gsumcom2  17199  dprdfadd  17255  dprdfsub  17256  dprdfeq0  17257  dprdf11  17258  dprdfaddOLD  17262  dprdfsubOLD  17263  dprdfeq0OLD  17264  dprdf11OLD  17265  dmdprdsplitlem  17279  dmdprdsplitlemOLD  17280  dprddisj2  17282  dprddisj2OLD  17283  dpjidcl  17302  dpjidclOLD  17309  ablfaclem2  17332  ablfac2  17335  mptscmfsuppd  17772  lmhmvsca  17886  rrgsupp  18134  rrgsuppOLD  18135  psrbagaddcl  18215  psrbagaddclOLD  18216  gsumbagdiaglem  18222  psrass1lem  18224  psrlinv  18245  psrass1  18255  psrcom  18259  mplsubrglem  18295  mplsubrglemOLD  18296  mplmonmul  18321  mplcoe1  18322  mplcoe5  18326  mplcoe2OLD  18328  evlslem2  18375  evlslem6  18376  evlslem6OLD  18377  evlslem1  18379  coe1fval3  18442  coe1sclmul  18518  coe1sclmul2  18520  ply1coeOLD  18533  mulgrhm2  18711  cygznlem2a  18779  frgpcyg  18785  uvcresum  18995  frlmup1  19000  grpvrinv  19065  mhmvlin  19066  mdetleib2  19257  mdetralt  19277  mdetunilem9  19289  cayleyhamilton1  19560  neiptopnei  19800  dfac14  20285  ptcnp  20289  lmcn2  20316  cnmpt11f  20331  cnmpt21f  20339  cnmpt2k  20355  qtopeu  20383  xkocnv  20481  xkohmeo  20482  flfcnp2  20674  istgp2  20756  tmdgsum  20760  symgtgp  20766  subgtgp  20770  tgpconcomp  20777  prdstgpd  20789  tsmsmhm  20814  tsmssub  20817  tgptsmscls  20818  tsmssplit  20820  tsmsxplem1  20821  tlmtgp  20864  ustuqtop  20915  prdsmslem1  21196  prdsxmslem1  21197  prdsxmslem2  21198  tngnm  21331  nmoeq0  21409  cnfldnm  21452  cncfmpt1f  21583  negfcncf  21589  cnrehmeo  21619  evth  21625  evth2  21626  copco  21684  pcopt  21688  pcopt2  21689  pcoass  21690  pcorev2  21694  pi1xfrcnv  21723  ovolctb  22067  ovolfs2  22146  uniioombllem2  22158  uniioombllem3  22160  ismbf  22203  mbfconst  22208  ismbfcn2  22212  mbfmulc2re  22221  mbfadd  22234  mbfsub  22235  mbflimsup  22239  itg1climres  22287  mbfi1flimlem  22295  mbfi1flim  22296  mbfmul  22299  itg2uba  22316  itg2mulclem  22319  itg2mulc  22320  itg2splitlem  22321  itg2monolem1  22323  itg2i1fseq  22328  itg2gt0  22333  itg2cnlem1  22334  itg2cnlem2  22335  i1fibl  22380  itgitg1  22381  iblabslem  22400  iblabs  22401  bddmulibl  22411  cnplimc  22457  limccnp  22461  limccnp2  22462  dvcnp2  22489  dvmulf  22512  dvcmulf  22514  dvcobr  22515  dvcof  22517  dvcjbr  22518  dvcj  22519  dvfre  22520  dvmptcj  22537  dvcnvlem  22543  dvcnv  22544  dvef  22547  dvsincos  22548  rolle  22557  cmvth  22558  dvlip  22560  dvlipcn  22561  dv11cn  22568  dvivthlem1  22575  dvivth  22577  lhop2  22582  dvfsumrlim2  22599  ftc1lem1  22602  ftc1lem2  22603  ftc1a  22604  ftc1lem4  22606  ftc2  22611  ftc2ditglem  22612  ftc2ditg  22613  tdeglem4  22624  tdeglem2  22625  mdegle0  22643  mdegmullem  22644  plypf1  22775  plyco  22804  dgrcolem1  22836  dgrcolem2  22837  dgrco  22838  plycjlem  22839  dvply2g  22847  plydiveu  22860  elqaalem3  22883  taylthlem1  22934  taylthlem2  22935  ulmshft  22951  ulmdvlem1  22961  mtest  22965  mtestbdd  22966  mbfulm  22967  iblulm  22968  itgulm  22969  pserulm  22983  pserdv  22990  abelthlem1  22992  abelthlem3  22994  pige3  23076  eff1olem  23101  logcn  23196  advlog  23203  advlogexp  23204  logtayl  23209  logccv  23212  dvcxp1  23284  dvcxp2  23285  resqrtcn  23291  sqrtcn  23292  loglesqrt  23300  dvatan  23463  leibpi  23470  divsqrtsumo1  23511  jensenlem2  23515  amgmlem  23517  ftalem7  23550  basellem9  23560  muinv  23667  dchrmulid2  23725  dchrinvcl  23726  lgseisenlem4  23825  dchrisum0lem2a  23900  logdivsum  23916  mulog2sumlem1  23917  log2sumbnd  23927  hilnormi  26278  chscllem4  26756  hmopidmchi  27268  rabfodom  27603  cofmpt  27731  ofoprabco  27732  fpwrelmapffslem  27786  fpwrelmap  27787  qqhre  28232  esumpcvgval  28307  ofcfval4  28334  omssubadd  28508  carsggect  28526  plymulx0  28768  lgamgulmlem2  28836  lgamcvg2  28861  ptpcon  28942  cvmliftlem6  28999  cvmliftlem8  29001  cvmlift2lem7  29018  cvmliftphtlem  29026  cvmlift3lem5  29032  elmsubrn  29152  mblfinlem2  30292  volsupnfl  30299  cnambfre  30303  dvtan  30305  itg2addnclem  30306  itg2addnclem2  30307  itg2addnclem3  30308  itg2addnc  30309  itg2gt0cn  30310  itgaddnc  30315  itgmulc2nc  30323  bddiblnc  30325  ftc1cnnclem  30328  ftc1anclem1  30330  ftc1anclem2  30331  ftc1anclem3  30332  ftc1anclem4  30333  ftc1anclem5  30334  ftc1anclem6  30335  ftc1anclem7  30336  ftc1anclem8  30337  ftc1anc  30338  ftc2nc  30339  dvcncxp1  30340  upixp  30460  mzpsubst  30920  diophun  30946  mendlmod  31383  mendassa  31384  binomcxplemnotnn0  31502  cncfmptss  31820  mulcncff  31909  subcncff  31921  cncfcompt  31924  addcncff  31926  divcncff  31933  cncfiooicclem1  31935  dvsinexp  31944  dvsubf  31948  dvdivf  31958  dvcosax  31962  dvnmul  31979  dvnprodlem1  31982  dvnprodlem2  31983  itgsinexplem1  31991  itgsubsticclem  32013  iblcncfioo  32016  itgiccshift  32018  stoweidlem20  32041  dirkercncflem2  32125  fourierdlem16  32144  fourierdlem21  32149  fourierdlem22  32150  fourierdlem28  32156  fourierdlem39  32167  fourierdlem51  32179  fourierdlem60  32188  fourierdlem61  32189  fourierdlem69  32197  fourierdlem72  32200  fourierdlem73  32201  fourierdlem81  32209  fourierdlem83  32211  fourierdlem84  32212  fourierdlem87  32215  fourierdlem90  32218  fourierdlem93  32221  fourierdlem95  32223  fourierdlem101  32229  fourierdlem103  32231  fourierdlem104  32232  fourierdlem111  32239  etransclem34  32290  etransclem43  32299  etransclem46  32302  aacllem  33604
  Copyright terms: Public domain W3C validator