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

Theorem feqmptd 6727
Description: Deduction form of dffn5 6718. (Contributed by Mario Carneiro, 8-Jan-2015.)
Hypothesis
Ref Expression
feqmptd.1 (𝜑𝐹:𝐴𝐵)
Assertion
Ref Expression
feqmptd (𝜑𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐹
Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)

Proof of Theorem feqmptd
StepHypRef Expression
1 feqmptd.1 . . 3 (𝜑𝐹:𝐴𝐵)
21ffnd 6509 . 2 (𝜑𝐹 Fn 𝐴)
3 dffn5 6718 . 2 (𝐹 Fn 𝐴𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
42, 3sylib 219 1 (𝜑𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  cmpt 5138   Fn wfn 6344  wf 6345  cfv 6349
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-fv 6357
This theorem is referenced by:  feqresmpt  6728  cofmpt  6887  fcoconst  6889  ofco  7418  caofinvl  7425  caofcom  7430  caofass  7432  caofdi  7434  caofdir  7435  caonncan  7436  suppssof1  7854  mapxpen  8672  xpmapenlem  8673  cantnfp1  9133  cantnflem1  9141  cnfcom2lem  9153  infxpenc  9433  pwfseqlem5  10074  gruf  10222  ccatco  14187  cnrecnv  14514  rlimclim1  14892  rlimuni  14897  lo1resb  14911  rlimresb  14912  o1resb  14913  rlimcn1  14935  rlimo1  14963  o1rlimmul  14965  caucvgr  15022  ackbijnn  15173  bitsf1ocnv  15783  ramcl  16355  pwsplusgval  16753  pwsmulrval  16754  pwsvscafval  16757  setcepi  17338  prf1st  17444  prf2nd  17445  1st2ndprf  17446  curfuncf  17478  curf2ndf  17487  yonedainv  17521  yonffthlem  17522  prdsidlem  17933  pwsco1mhm  17986  pwsco2mhm  17987  frmdup3lem  18021  frmdup3  18022  grpinvcnv  18107  pwsinvg  18152  pwssub  18153  efginvrel1  18785  frgpup3lem  18834  frgpup3  18835  gsumval3  18958  gsumcllem  18959  gsumzf1o  18963  gsumzsplit  18978  gsumconst  18985  gsumzmhm  18988  gsumsub  18999  gsum2dlem2  19022  gsumcom2  19026  dprdfadd  19073  dprdfsub  19074  dprdfeq0  19075  dprdf11  19076  dmdprdsplitlem  19090  dprddisj2  19092  dpjidcl  19111  ablfaclem2  19139  ablfac2  19142  mptscmfsuppd  19631  lmhmvsca  19748  rrgsupp  19994  psrbagaddcl  20080  gsumbagdiaglem  20085  psrass1lem  20087  psrlinv  20107  psrass1  20115  psrcom  20119  mplsubrglem  20149  mplmonmul  20175  mplcoe1  20176  mplcoe5  20179  evlslem2  20222  evlslem6  20224  evlslem1  20225  coe1fval3  20306  coe1sclmul  20380  coe1sclmul2  20382  mulgrhm2  20576  cygznlem2a  20644  frgpcyg  20650  uvcresum  20867  frlmup1  20872  grpvrinv  20937  mhmvlin  20938  mdetleib2  21127  mdetunilem9  21159  cayleyhamilton1  21430  neiptopnei  21670  dfac14  22156  ptcnp  22160  lmcn2  22187  cnmpt11f  22202  cnmpt21f  22210  cnmpt2k  22226  qtopeu  22254  xkocnv  22352  xkohmeo  22353  flfcnp2  22545  istgp2  22629  tmdgsum  22633  symgtgp  22639  subgtgp  22643  tgpconncomp  22650  prdstgpd  22662  tsmssub  22686  tgptsmscls  22687  tsmssplit  22689  tsmsxplem1  22690  tlmtgp  22733  ustuqtop  22784  prdsmslem1  23066  prdsxmslem1  23067  prdsxmslem2  23068  tngnm  23189  nmoeq0  23274  cnfldnm  23316  cncfmpt1f  23450  negfcncf  23456  cnrehmeo  23486  evth  23492  evth2  23493  copco  23551  pcopt  23555  pcopt2  23556  pcoass  23557  pcorev2  23561  pi1xfrcnv  23590  ovolctb  24020  ovolfs2  24101  uniioombllem2  24113  ismbf  24158  mbfconst  24163  mbfmulc2re  24178  mbfadd  24191  mbfsub  24192  mbflimsup  24196  mbfi1flimlem  24252  mbfi1flim  24253  mbfmul  24256  itg2uba  24273  itg2mulclem  24276  itg2mulc  24277  itg2splitlem  24278  itg2monolem1  24280  itg2i1fseq  24285  itg2gt0  24290  itg2cnlem1  24291  itg2cnlem2  24292  i1fibl  24337  itgitg1  24338  bddmulibl  24368  cnplimc  24414  limccnp2  24419  dvcnp2  24446  dvmulf  24469  dvcmulf  24471  dvcobr  24472  dvcof  24474  dvcj  24476  dvfre  24477  dvmptcj  24494  dvcnvlem  24502  dvcnv  24503  dvef  24506  dvsincos  24507  rolle  24516  cmvth  24517  dvlip  24519  dvlipcn  24520  dv11cn  24527  dvivthlem1  24534  dvivth  24536  lhop2  24541  dvfsumrlim2  24558  ftc1lem1  24561  ftc1lem2  24562  ftc1a  24563  ftc1lem4  24565  ftc2  24570  ftc2ditglem  24571  ftc2ditg  24572  tdeglem4  24583  tdeglem2  24584  mdegle0  24600  mdegmullem  24601  plypf1  24731  plyco  24760  dgrcolem1  24792  dgrcolem2  24793  dgrco  24794  plycjlem  24795  dvply2g  24803  plydiveu  24816  elqaalem3  24839  taylthlem1  24890  taylthlem2  24891  ulmshft  24907  ulmdvlem1  24917  mtest  24921  mtestbdd  24922  mbfulm  24923  iblulm  24924  itgulm  24925  pserulm  24939  pserdv  24946  abelthlem1  24948  abelthlem3  24950  pige3ALT  25034  eff1olem  25059  logcn  25157  advlog  25164  advlogexp  25165  logtayl  25170  logccv  25173  dvcxp1  25248  dvcxp2  25249  dvcncxp1  25251  resqrtcn  25257  sqrtcn  25258  loglesqrt  25266  dvatan  25440  leibpi  25448  divsqrtsumo1  25489  jensenlem2  25493  amgmlem  25495  lgamgulmlem2  25535  ftalem7  25584  basellem9  25594  muinv  25698  dchrmulid2  25756  dchrinvcl  25757  dchrisum0lem2a  26021  logdivsum  26037  mulog2sumlem1  26038  log2sumbnd  26048  hilnormi  28868  chscllem4  29345  hmopidmchi  29856  rabfodom  30194  ofoprabco  30338  fpwrelmapffslem  30395  fpwrelmap  30396  lbsdiflsp0  30922  fedgmullem1  30925  qqhre  31161  prodindf  31182  esumpcvgval  31237  ofcfval4  31264  omssubadd  31458  carsggect  31476  plymulx0  31717  fdvneggt  31771  fdvnegge  31773  itgexpif  31777  ptpconn  32378  cvmliftlem6  32435  cvmliftlem8  32437  cvmlift2lem7  32454  cvmliftphtlem  32462  cvmlift3lem5  32468  elmsubrn  32673  knoppcnlem9  33738  curunc  34756  poimir  34807  broucube  34808  mblfinlem2  34812  volsupnfl  34819  cnambfre  34822  dvtan  34824  itg2addnclem  34825  itg2addnclem2  34826  itg2addnclem3  34827  itg2addnc  34828  itg2gt0cn  34829  itgaddnc  34834  itgmulc2nc  34842  bddiblnc  34844  ftc1cnnclem  34847  ftc1anclem1  34849  ftc1anclem2  34850  ftc1anclem3  34851  ftc1anclem4  34852  ftc1anclem5  34853  ftc1anclem6  34854  ftc1anclem7  34855  ftc1anclem8  34856  ftc1anc  34857  ftc2nc  34858  upixp  34887  mzpsubst  39225  diophun  39250  mendlmod  39673  mendassa  39674  fsovcnvlem  40239  binomcxplemnotnn0  40568  rnsnf  41324  cncfmptss  41748  climliminflimsupd  41962  mulcncff  42031  subcncff  42043  cncfcompt  42046  addcncff  42047  divcncff  42054  cncfiooicclem1  42056  dvsinexp  42075  dvsubf  42078  dvdivf  42087  dvcosax  42091  dvnmul  42108  dvnprodlem1  42111  dvnprodlem2  42112  itgsinexplem1  42119  itgsubsticclem  42140  iblcncfioo  42143  itgiccshift  42145  stoweidlem20  42186  dirkercncflem2  42270  fourierdlem16  42289  fourierdlem21  42294  fourierdlem22  42295  fourierdlem28  42301  fourierdlem39  42312  fourierdlem51  42323  fourierdlem60  42332  fourierdlem61  42333  fourierdlem69  42341  fourierdlem72  42344  fourierdlem73  42345  fourierdlem81  42353  fourierdlem83  42355  fourierdlem84  42356  fourierdlem87  42359  fourierdlem90  42362  fourierdlem93  42365  fourierdlem95  42367  fourierdlem101  42373  fourierdlem103  42375  fourierdlem104  42376  fourierdlem111  42383  etransclem34  42434  etransclem43  42443  etransclem46  42446  sge0tsms  42543  sge0fodjrnlem  42579  sge0iun  42582  sge0isum  42590  sge0seq  42609  meadjun  42625  meadjiunlem  42628  meadjiun  42629  ismeannd  42630  psmeasurelem  42633  omeiunle  42680  ovn02  42731  smfpimioo  42943  smfresal  42944  smfinflem  42972  smflimsuplem3  42977  smfliminflem  42985  aacllem  44800  amgmwlem  44801  amgmlemALT  44802
  Copyright terms: Public domain W3C validator