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

Theorem feqmptd 6473
Description: Deduction form of dffn5 6465. (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 6260 . 2 (𝜑𝐹 Fn 𝐴)
3 dffn5 6465 . 2 (𝐹 Fn 𝐴𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
42, 3sylib 209 1 (𝜑𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  cmpt 4930   Fn wfn 6099  wf 6100  cfv 6104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-sep 4982  ax-nul 4990  ax-pr 5103
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3400  df-sbc 3641  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-nul 4124  df-if 4287  df-sn 4378  df-pr 4380  df-op 4384  df-uni 4638  df-br 4852  df-opab 4914  df-mpt 4931  df-id 5226  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-iota 6067  df-fun 6106  df-fn 6107  df-f 6108  df-fv 6112
This theorem is referenced by:  feqresmpt  6474  cofmpt  6625  fcoconst  6627  ofco  7150  caofinvl  7157  caofcom  7162  caofass  7164  caofdi  7166  caofdir  7167  caonncan  7168  suppssof1  7566  mapxpen  8368  xpmapenlem  8369  cantnfp1  8828  cantnflem1  8836  cnfcom2lem  8848  infxpenc  9127  pwfseqlem5  9773  gruf  9921  ccatco  13808  cnrecnv  14131  lo1o12  14490  rlimclim1  14502  rlimuni  14507  lo1resb  14521  rlimresb  14522  o1resb  14523  rlimcn1  14545  rlimcn1b  14546  rlimo1  14573  o1rlimmul  14575  caucvgr  14632  ackbijnn  14785  bitsf1ocnv  15388  ramcl  15953  pwsplusgval  16358  pwsmulrval  16359  pwsvscafval  16362  setcepi  16945  prf1st  17052  prf2nd  17053  1st2ndprf  17054  curfuncf  17086  curf2ndf  17095  yonedainv  17129  yonffthlem  17130  prdsidlem  17530  pwsco1mhm  17578  pwsco2mhm  17579  frmdup3lem  17611  frmdup3  17612  grpinvcnv  17691  pwsinvg  17736  pwssub  17737  psgnunilem5  18118  efginvrel1  18345  frgpup3lem  18394  frgpup3  18395  gsumval3  18512  gsumcllem  18513  gsumzf1o  18517  gsumzsplit  18531  gsumconst  18538  gsumzmhm  18541  gsumsub  18552  gsum2dlem2  18574  gsumcom2  18578  dprdfadd  18624  dprdfsub  18625  dprdfeq0  18626  dprdf11  18627  dmdprdsplitlem  18641  dprddisj2  18643  dpjidcl  18662  ablfaclem2  18690  ablfac2  18693  mptscmfsuppd  19136  lmhmvsca  19255  rrgsupp  19503  psrbagaddcl  19582  gsumbagdiaglem  19587  psrass1lem  19589  psrlinv  19609  psrass1  19617  psrcom  19621  mplsubrglem  19651  mplmonmul  19676  mplcoe1  19677  mplcoe5  19680  evlslem2  19723  evlslem6  19724  evlslem1  19726  coe1fval3  19789  coe1sclmul  19863  coe1sclmul2  19865  mulgrhm2  20058  cygznlem2a  20126  frgpcyg  20132  uvcresum  20346  frlmup1  20351  grpvrinv  20416  mhmvlin  20417  mdetleib2  20609  mdetralt  20629  mdetunilem9  20641  cayleyhamilton1  20914  neiptopnei  21154  dfac14  21639  ptcnp  21643  lmcn2  21670  cnmpt11f  21685  cnmpt21f  21693  cnmpt2k  21709  qtopeu  21737  xkocnv  21835  xkohmeo  21836  flfcnp2  22028  istgp2  22112  tmdgsum  22116  symgtgp  22122  subgtgp  22126  tgpconncomp  22133  prdstgpd  22145  tsmsmhm  22166  tsmssub  22169  tgptsmscls  22170  tsmssplit  22172  tsmsxplem1  22173  tlmtgp  22216  ustuqtop  22267  prdsmslem1  22549  prdsxmslem1  22550  prdsxmslem2  22551  tngnm  22672  nmoeq0  22757  cnfldnm  22799  cncfmpt1f  22933  negfcncf  22939  cnrehmeo  22969  evth  22975  evth2  22976  copco  23034  pcopt  23038  pcopt2  23039  pcoass  23040  pcorev2  23044  pi1xfrcnv  23073  ovolctb  23477  ovolfs2  23558  uniioombllem2  23570  uniioombllem3  23572  ismbf  23615  mbfconst  23620  ismbfcn2  23625  mbfmulc2re  23635  mbfadd  23648  mbfsub  23649  mbflimsup  23653  itg1climres  23701  mbfi1flimlem  23709  mbfi1flim  23710  mbfmul  23713  itg2uba  23730  itg2mulclem  23733  itg2mulc  23734  itg2splitlem  23735  itg2monolem1  23737  itg2i1fseq  23742  itg2gt0  23747  itg2cnlem1  23748  itg2cnlem2  23749  i1fibl  23794  itgitg1  23795  iblabslem  23814  iblabs  23815  bddmulibl  23825  cnplimc  23871  limccnp  23875  limccnp2  23876  dvcnp2  23903  dvmulf  23926  dvcmulf  23928  dvcobr  23929  dvcof  23931  dvcjbr  23932  dvcj  23933  dvfre  23934  dvmptcj  23951  dvcnvlem  23959  dvcnv  23960  dvef  23963  dvsincos  23964  rolle  23973  cmvth  23974  dvlip  23976  dvlipcn  23977  dv11cn  23984  dvivthlem1  23991  dvivth  23993  lhop2  23998  dvfsumrlim2  24015  ftc1lem1  24018  ftc1lem2  24019  ftc1a  24020  ftc1lem4  24022  ftc2  24027  ftc2ditglem  24028  ftc2ditg  24029  tdeglem4  24040  tdeglem2  24041  mdegle0  24057  mdegmullem  24058  plypf1  24188  plyco  24217  dgrcolem1  24249  dgrcolem2  24250  dgrco  24251  plycjlem  24252  dvply2g  24260  plydiveu  24273  elqaalem3  24296  taylthlem1  24347  taylthlem2  24348  ulmshft  24364  ulmdvlem1  24374  mtest  24378  mtestbdd  24379  mbfulm  24380  iblulm  24381  itgulm  24382  pserulm  24396  pserdv  24403  abelthlem1  24405  abelthlem3  24407  pige3  24490  eff1olem  24515  logcn  24613  advlog  24620  advlogexp  24621  logtayl  24626  logccv  24629  dvcxp1  24701  dvcxp2  24702  dvcncxp1  24704  resqrtcn  24710  sqrtcn  24711  loglesqrt  24719  dvatan  24882  leibpi  24889  divsqrtsumo1  24930  jensenlem2  24934  amgmlem  24936  lgamgulmlem2  24976  lgamcvg2  25001  ftalem7  25025  basellem9  25035  muinv  25139  dchrmulid2  25197  dchrinvcl  25198  lgseisenlem4  25323  dchrisum0lem2a  25426  logdivsum  25442  mulog2sumlem1  25443  log2sumbnd  25453  hilnormi  28354  chscllem4  28833  hmopidmchi  29344  rabfodom  29675  ofoprabco  29797  fpwrelmapffslem  29840  fpwrelmap  29841  qqhre  30395  prodindf  30416  esumpcvgval  30471  ofcfval4  30498  omssubadd  30693  carsggect  30711  plymulx0  30955  fdvneggt  31009  fdvnegge  31011  itgexpif  31015  ptpconn  31543  cvmliftlem6  31600  cvmliftlem8  31602  cvmlift2lem7  31619  cvmliftphtlem  31627  cvmlift3lem5  31633  elmsubrn  31753  knoppcnlem9  32813  curunc  33706  poimir  33757  broucube  33758  mblfinlem2  33762  volsupnfl  33769  cnambfre  33772  dvtan  33774  itg2addnclem  33775  itg2addnclem2  33776  itg2addnclem3  33777  itg2addnc  33778  itg2gt0cn  33779  itgaddnc  33784  itgmulc2nc  33792  bddiblnc  33794  ftc1cnnclem  33797  ftc1anclem1  33799  ftc1anclem2  33800  ftc1anclem3  33801  ftc1anclem4  33802  ftc1anclem5  33803  ftc1anclem6  33804  ftc1anclem7  33805  ftc1anclem8  33806  ftc1anc  33807  ftc2nc  33808  upixp  33838  mzpsubst  37814  diophun  37840  mendlmod  38265  mendassa  38266  fsovcnvlem  38808  binomcxplemnotnn0  39056  rnsnf  39860  cncfmptss  40300  climliminflimsupd  40514  mulcncff  40562  subcncff  40574  cncfcompt  40577  addcncff  40578  divcncff  40585  cncfiooicclem1  40587  dvsinexp  40606  dvsubf  40609  dvdivf  40618  dvcosax  40622  dvnmul  40639  dvnprodlem1  40642  dvnprodlem2  40643  itgsinexplem1  40650  itgsubsticclem  40671  iblcncfioo  40674  itgiccshift  40676  stoweidlem20  40717  dirkercncflem2  40801  fourierdlem16  40820  fourierdlem21  40825  fourierdlem22  40826  fourierdlem28  40832  fourierdlem39  40843  fourierdlem51  40854  fourierdlem60  40863  fourierdlem61  40864  fourierdlem69  40872  fourierdlem72  40875  fourierdlem73  40876  fourierdlem81  40884  fourierdlem83  40886  fourierdlem84  40887  fourierdlem87  40890  fourierdlem90  40893  fourierdlem93  40896  fourierdlem95  40898  fourierdlem101  40904  fourierdlem103  40906  fourierdlem104  40907  fourierdlem111  40914  etransclem34  40965  etransclem43  40974  etransclem46  40977  sge0tsms  41077  sge0fodjrnlem  41113  sge0iun  41116  sge0isum  41124  sge0seq  41143  meadjun  41159  meadjiunlem  41162  meadjiun  41163  ismeannd  41164  psmeasurelem  41167  omeiunle  41214  ovn02  41265  smfpimioo  41477  smfresal  41478  smfinflem  41506  smflimsuplem3  41511  smfliminflem  41519  aacllem  43119  amgmwlem  43120  amgmlemALT  43121
  Copyright terms: Public domain W3C validator