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

Theorem feqmptd 5918
Description: Deduction form of dffn5 5910. (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 5728 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
31, 2syl 17 . 2  |-  ( ph  ->  F  Fn  A )
4 dffn5 5910 . 2  |-  ( F  Fn  A  <->  F  =  ( x  e.  A  |->  ( F `  x
) ) )
53, 4sylib 200 1  |-  ( ph  ->  F  =  ( x  e.  A  |->  ( F `
 x ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1444    |-> cmpt 4461    Fn wfn 5577   -->wf 5578   ` cfv 5582
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pr 4639
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-fv 5590
This theorem is referenced by:  feqresmpt  5919  fcoconst  6060  ofco  6551  caofinvl  6558  caofcom  6563  caofass  6565  caofdi  6567  caofdir  6568  caonncan  6569  suppssof1  6948  mapxpen  7738  xpmapenlem  7739  cantnfp1  8186  cantnflem1  8194  cnfcom2lem  8206  infxpenc  8449  pwfseqlem5  9088  gruf  9236  ccatco  12932  cnrecnv  13228  lo1o12  13597  rlimclim1  13609  rlimuni  13614  lo1resb  13628  rlimresb  13629  o1resb  13630  rlimcn1  13652  rlimcn1b  13653  rlimo1  13680  o1rlimmul  13682  caucvgr  13741  ackbijnn  13886  bitsf1ocnv  14418  ramcl  14987  pwsplusgval  15388  pwsmulrval  15389  pwsvscafval  15392  setcepi  15983  prf1st  16089  prf2nd  16090  1st2ndprf  16091  curfuncf  16123  curf2ndf  16132  yonedainv  16166  yonffthlem  16167  prdsidlem  16568  pwsco1mhm  16617  pwsco2mhm  16618  frmdup3lem  16650  frmdup3  16651  grpinvcnv  16722  pwsinvg  16798  pwssub  16799  psgnunilem5  17135  efginvrel1  17378  frgpup3lem  17427  frgpup3  17428  gsumval3  17541  gsumcllem  17542  gsumzf1o  17546  gsumzsplit  17560  gsumconst  17567  gsumzmhm  17570  gsumsub  17581  gsum2dlem2  17603  gsumcom2  17607  dprdfadd  17653  dprdfsub  17654  dprdfeq0  17655  dprdf11  17656  dmdprdsplitlem  17670  dprddisj2  17672  dpjidcl  17691  ablfaclem2  17719  ablfac2  17722  mptscmfsuppd  18154  lmhmvsca  18268  rrgsupp  18515  psrbagaddcl  18594  gsumbagdiaglem  18599  psrass1lem  18601  psrlinv  18621  psrass1  18629  psrcom  18633  mplsubrglem  18663  mplmonmul  18688  mplcoe1  18689  mplcoe5  18692  evlslem2  18735  evlslem6  18736  evlslem1  18738  coe1fval3  18801  coe1sclmul  18875  coe1sclmul2  18877  ply1coeOLD  18890  mulgrhm2  19070  cygznlem2a  19138  frgpcyg  19144  uvcresum  19351  frlmup1  19356  grpvrinv  19421  mhmvlin  19422  mdetleib2  19613  mdetralt  19633  mdetunilem9  19645  cayleyhamilton1  19916  neiptopnei  20148  dfac14  20633  ptcnp  20637  lmcn2  20664  cnmpt11f  20679  cnmpt21f  20687  cnmpt2k  20703  qtopeu  20731  xkocnv  20829  xkohmeo  20830  flfcnp2  21022  istgp2  21106  tmdgsum  21110  symgtgp  21116  subgtgp  21120  tgpconcomp  21127  prdstgpd  21139  tsmsmhm  21160  tsmssub  21163  tgptsmscls  21164  tsmssplit  21166  tsmsxplem1  21167  tlmtgp  21210  ustuqtop  21261  prdsmslem1  21542  prdsxmslem1  21543  prdsxmslem2  21544  tngnm  21659  nmoeq0  21757  cnfldnm  21799  cncfmpt1f  21945  negfcncf  21951  cnrehmeo  21981  evth  21987  evth2  21988  copco  22049  pcopt  22053  pcopt2  22054  pcoass  22055  pcorev2  22059  pi1xfrcnv  22088  ovolctb  22443  ovolfs2  22523  uniioombllem2  22540  uniioombllem2OLD  22541  uniioombllem3  22543  ismbf  22586  mbfconst  22591  ismbfcn2  22595  mbfmulc2re  22604  mbfadd  22617  mbfsub  22618  mbflimsup  22623  mbflimsupOLD  22624  itg1climres  22672  mbfi1flimlem  22680  mbfi1flim  22681  mbfmul  22684  itg2uba  22701  itg2mulclem  22704  itg2mulc  22705  itg2splitlem  22706  itg2monolem1  22708  itg2i1fseq  22713  itg2gt0  22718  itg2cnlem1  22719  itg2cnlem2  22720  i1fibl  22765  itgitg1  22766  iblabslem  22785  iblabs  22786  bddmulibl  22796  cnplimc  22842  limccnp  22846  limccnp2  22847  dvcnp2  22874  dvmulf  22897  dvcmulf  22899  dvcobr  22900  dvcof  22902  dvcjbr  22903  dvcj  22904  dvfre  22905  dvmptcj  22922  dvcnvlem  22928  dvcnv  22929  dvef  22932  dvsincos  22933  rolle  22942  cmvth  22943  dvlip  22945  dvlipcn  22946  dv11cn  22953  dvivthlem1  22960  dvivth  22962  lhop2  22967  dvfsumrlim2  22984  ftc1lem1  22987  ftc1lem2  22988  ftc1a  22989  ftc1lem4  22991  ftc2  22996  ftc2ditglem  22997  ftc2ditg  22998  tdeglem4  23009  tdeglem2  23010  mdegle0  23026  mdegmullem  23027  plypf1  23166  plyco  23195  dgrcolem1  23227  dgrcolem2  23228  dgrco  23229  plycjlem  23230  dvply2g  23238  plydiveu  23251  elqaalem3  23274  elqaalem3OLD  23277  taylthlem1  23328  taylthlem2  23329  ulmshft  23345  ulmdvlem1  23355  mtest  23359  mtestbdd  23360  mbfulm  23361  iblulm  23362  itgulm  23363  pserulm  23377  pserdv  23384  abelthlem1  23386  abelthlem3  23388  pige3  23472  eff1olem  23497  logcn  23592  advlog  23599  advlogexp  23600  logtayl  23605  logccv  23608  dvcxp1  23680  dvcxp2  23681  dvcncxp1  23683  resqrtcn  23689  sqrtcn  23690  loglesqrt  23698  dvatan  23861  leibpi  23868  divsqrtsumo1  23909  jensenlem2  23913  amgmlem  23915  lgamgulmlem2  23955  lgamcvg2  23980  ftalem7  24005  basellem9  24015  muinv  24122  dchrmulid2  24180  dchrinvcl  24181  lgseisenlem4  24280  dchrisum0lem2a  24355  logdivsum  24371  mulog2sumlem1  24372  log2sumbnd  24382  hilnormi  26816  chscllem4  27293  hmopidmchi  27804  rabfodom  28140  cofmpt  28266  ofoprabco  28267  fpwrelmapffslem  28317  fpwrelmap  28318  qqhre  28824  esumpcvgval  28899  ofcfval4  28926  omssubadd  29128  omssubaddOLD  29132  carsggect  29150  plymulx0  29436  ptpcon  29956  cvmliftlem6  30013  cvmliftlem8  30015  cvmlift2lem7  30032  cvmliftphtlem  30040  cvmlift3lem5  30046  elmsubrn  30166  poimir  31973  broucube  31974  mblfinlem2  31978  volsupnfl  31985  cnambfre  31989  dvtan  31992  itg2addnclem  31993  itg2addnclem2  31994  itg2addnclem3  31995  itg2addnc  31996  itg2gt0cn  31997  itgaddnc  32002  itgmulc2nc  32010  bddiblnc  32012  ftc1cnnclem  32015  ftc1anclem1  32017  ftc1anclem2  32018  ftc1anclem3  32019  ftc1anclem4  32020  ftc1anclem5  32021  ftc1anclem6  32022  ftc1anclem7  32023  ftc1anclem8  32024  ftc1anc  32025  ftc2nc  32026  upixp  32056  mzpsubst  35590  diophun  35616  mendlmod  36059  mendassa  36060  binomcxplemnotnn0  36705  rnsnf  37458  cncfmptss  37665  mulcncff  37745  subcncff  37757  cncfcompt  37760  addcncff  37762  divcncff  37769  cncfiooicclem1  37771  dvsinexp  37780  dvsubf  37784  dvdivf  37794  dvcosax  37798  dvnmul  37818  dvnprodlem1  37821  dvnprodlem2  37822  itgsinexplem1  37830  itgsubsticclem  37852  iblcncfioo  37855  itgiccshift  37857  stoweidlem20  37880  dirkercncflem2  37966  fourierdlem16  37985  fourierdlem21  37990  fourierdlem22  37991  fourierdlem28  37997  fourierdlem39  38009  fourierdlem51  38021  fourierdlem60  38030  fourierdlem61  38031  fourierdlem69  38039  fourierdlem72  38042  fourierdlem73  38043  fourierdlem81  38051  fourierdlem83  38053  fourierdlem84  38054  fourierdlem87  38057  fourierdlem90  38060  fourierdlem93  38063  fourierdlem95  38065  fourierdlem101  38071  fourierdlem103  38073  fourierdlem104  38074  fourierdlem111  38081  etransclem34  38133  etransclem43  38142  etransclem46  38145  sge0tsms  38222  sge0fodjrnlem  38258  sge0iun  38261  sge0isum  38269  meadjun  38300  meadjiunlem  38303  meadjiun  38304  ismeannd  38305  psmeasurelem  38308  omeiunle  38338  ovn02  38390  aacllem  40593
  Copyright terms: Public domain W3C validator