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

Theorem feqmptd 6144
Description: Deduction form of dffn5 6136. (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 (𝜑𝐹:𝐴𝐵)
2 ffn 5944 . . 3 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
31, 2syl 17 . 2 (𝜑𝐹 Fn 𝐴)
4 dffn5 6136 . 2 (𝐹 Fn 𝐴𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
53, 4sylib 206 1 (𝜑𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  cmpt 4637   Fn wfn 5785  wf 5786  cfv 5790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pr 4828
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-fv 5798
This theorem is referenced by:  feqresmpt  6145  fcoconst  6292  ofco  6793  caofinvl  6800  caofcom  6805  caofass  6807  caofdi  6809  caofdir  6810  caonncan  6811  suppssof1  7193  mapxpen  7989  xpmapenlem  7990  cantnfp1  8439  cantnflem1  8447  cnfcom2lem  8459  infxpenc  8702  pwfseqlem5  9342  gruf  9490  ccatco  13381  cnrecnv  13702  lo1o12  14061  rlimclim1  14073  rlimuni  14078  lo1resb  14092  rlimresb  14093  o1resb  14094  rlimcn1  14116  rlimcn1b  14117  rlimo1  14144  o1rlimmul  14146  caucvgr  14203  ackbijnn  14348  bitsf1ocnv  14953  ramcl  15520  pwsplusgval  15922  pwsmulrval  15923  pwsvscafval  15926  setcepi  16510  prf1st  16616  prf2nd  16617  1st2ndprf  16618  curfuncf  16650  curf2ndf  16659  yonedainv  16693  yonffthlem  16694  prdsidlem  17094  pwsco1mhm  17142  pwsco2mhm  17143  frmdup3lem  17175  frmdup3  17176  grpinvcnv  17255  pwsinvg  17300  pwssub  17301  psgnunilem5  17686  efginvrel1  17913  frgpup3lem  17962  frgpup3  17963  gsumval3  18080  gsumcllem  18081  gsumzf1o  18085  gsumzsplit  18099  gsumconst  18106  gsumzmhm  18109  gsumsub  18120  gsum2dlem2  18142  gsumcom2  18146  dprdfadd  18191  dprdfsub  18192  dprdfeq0  18193  dprdf11  18194  dmdprdsplitlem  18208  dprddisj2  18210  dpjidcl  18229  ablfaclem2  18257  ablfac2  18260  mptscmfsuppd  18701  lmhmvsca  18815  rrgsupp  19061  psrbagaddcl  19140  gsumbagdiaglem  19145  psrass1lem  19147  psrlinv  19167  psrass1  19175  psrcom  19179  mplsubrglem  19209  mplmonmul  19234  mplcoe1  19235  mplcoe5  19238  evlslem2  19282  evlslem6  19283  evlslem1  19285  coe1fval3  19348  coe1sclmul  19422  coe1sclmul2  19424  mulgrhm2  19614  cygznlem2a  19683  frgpcyg  19689  uvcresum  19899  frlmup1  19904  grpvrinv  19969  mhmvlin  19970  mdetleib2  20161  mdetralt  20181  mdetunilem9  20193  cayleyhamilton1  20464  neiptopnei  20694  dfac14  21179  ptcnp  21183  lmcn2  21210  cnmpt11f  21225  cnmpt21f  21233  cnmpt2k  21249  qtopeu  21277  xkocnv  21375  xkohmeo  21376  flfcnp2  21569  istgp2  21653  tmdgsum  21657  symgtgp  21663  subgtgp  21667  tgpconcomp  21674  prdstgpd  21686  tsmsmhm  21707  tsmssub  21710  tgptsmscls  21711  tsmssplit  21713  tsmsxplem1  21714  tlmtgp  21757  ustuqtop  21808  prdsmslem1  22090  prdsxmslem1  22091  prdsxmslem2  22092  tngnm  22213  nmoeq0  22298  cnfldnm  22340  cncfmpt1f  22472  negfcncf  22478  cnrehmeo  22508  evth  22514  evth2  22515  copco  22574  pcopt  22578  pcopt2  22579  pcoass  22580  pcorev2  22584  pi1xfrcnv  22613  ovolctb  23010  ovolfs2  23090  uniioombllem2  23102  uniioombllem3  23104  ismbf  23148  mbfconst  23153  ismbfcn2  23157  mbfmulc2re  23166  mbfadd  23179  mbfsub  23180  mbflimsup  23184  itg1climres  23232  mbfi1flimlem  23240  mbfi1flim  23241  mbfmul  23244  itg2uba  23261  itg2mulclem  23264  itg2mulc  23265  itg2splitlem  23266  itg2monolem1  23268  itg2i1fseq  23273  itg2gt0  23278  itg2cnlem1  23279  itg2cnlem2  23280  i1fibl  23325  itgitg1  23326  iblabslem  23345  iblabs  23346  bddmulibl  23356  cnplimc  23402  limccnp  23406  limccnp2  23407  dvcnp2  23434  dvmulf  23457  dvcmulf  23459  dvcobr  23460  dvcof  23462  dvcjbr  23463  dvcj  23464  dvfre  23465  dvmptcj  23482  dvcnvlem  23488  dvcnv  23489  dvef  23492  dvsincos  23493  rolle  23502  cmvth  23503  dvlip  23505  dvlipcn  23506  dv11cn  23513  dvivthlem1  23520  dvivth  23522  lhop2  23527  dvfsumrlim2  23544  ftc1lem1  23547  ftc1lem2  23548  ftc1a  23549  ftc1lem4  23551  ftc2  23556  ftc2ditglem  23557  ftc2ditg  23558  tdeglem4  23569  tdeglem2  23570  mdegle0  23586  mdegmullem  23587  plypf1  23717  plyco  23746  dgrcolem1  23778  dgrcolem2  23779  dgrco  23780  plycjlem  23781  dvply2g  23789  plydiveu  23802  elqaalem3  23825  taylthlem1  23876  taylthlem2  23877  ulmshft  23893  ulmdvlem1  23903  mtest  23907  mtestbdd  23908  mbfulm  23909  iblulm  23910  itgulm  23911  pserulm  23925  pserdv  23932  abelthlem1  23934  abelthlem3  23936  pige3  24018  eff1olem  24043  logcn  24138  advlog  24145  advlogexp  24146  logtayl  24151  logccv  24154  dvcxp1  24226  dvcxp2  24227  dvcncxp1  24229  resqrtcn  24235  sqrtcn  24236  loglesqrt  24244  dvatan  24407  leibpi  24414  divsqrtsumo1  24455  jensenlem2  24459  amgmlem  24461  lgamgulmlem2  24501  lgamcvg2  24526  ftalem7  24550  basellem9  24560  muinv  24664  dchrmulid2  24722  dchrinvcl  24723  lgseisenlem4  24848  dchrisum0lem2a  24951  logdivsum  24967  mulog2sumlem1  24968  log2sumbnd  24978  hilnormi  27238  chscllem4  27717  hmopidmchi  28228  rabfodom  28562  cofmpt  28680  ofoprabco  28681  fpwrelmapffslem  28729  fpwrelmap  28730  qqhre  29226  esumpcvgval  29301  ofcfval4  29328  omssubadd  29523  carsggect  29541  plymulx0  29784  ptpcon  30303  cvmliftlem6  30360  cvmliftlem8  30362  cvmlift2lem7  30379  cvmliftphtlem  30387  cvmlift3lem5  30393  elmsubrn  30513  knoppcnlem9  31495  curunc  32385  poimir  32436  broucube  32437  mblfinlem2  32441  volsupnfl  32448  cnambfre  32452  dvtan  32454  itg2addnclem  32455  itg2addnclem2  32456  itg2addnclem3  32457  itg2addnc  32458  itg2gt0cn  32459  itgaddnc  32464  itgmulc2nc  32472  bddiblnc  32474  ftc1cnnclem  32477  ftc1anclem1  32479  ftc1anclem2  32480  ftc1anclem3  32481  ftc1anclem4  32482  ftc1anclem5  32483  ftc1anclem6  32484  ftc1anclem7  32485  ftc1anclem8  32486  ftc1anc  32487  ftc2nc  32488  upixp  32518  mzpsubst  36153  diophun  36179  mendlmod  36606  mendassa  36607  fsovcnvlem  37151  binomcxplemnotnn0  37401  rnsnf  38189  cncfmptss  38478  mulcncff  38577  subcncff  38589  cncfcompt  38592  addcncff  38594  divcncff  38601  cncfiooicclem1  38603  dvsinexp  38622  dvsubf  38626  dvdivf  38636  dvcosax  38640  dvnmul  38657  dvnprodlem1  38660  dvnprodlem2  38661  itgsinexplem1  38669  itgsubsticclem  38691  iblcncfioo  38694  itgiccshift  38696  stoweidlem20  38737  dirkercncflem2  38821  fourierdlem16  38840  fourierdlem21  38845  fourierdlem22  38846  fourierdlem28  38852  fourierdlem39  38863  fourierdlem51  38874  fourierdlem60  38883  fourierdlem61  38884  fourierdlem69  38892  fourierdlem72  38895  fourierdlem73  38896  fourierdlem81  38904  fourierdlem83  38906  fourierdlem84  38907  fourierdlem87  38910  fourierdlem90  38913  fourierdlem93  38916  fourierdlem95  38918  fourierdlem101  38924  fourierdlem103  38926  fourierdlem104  38927  fourierdlem111  38934  etransclem34  38985  etransclem43  38994  etransclem46  38997  sge0tsms  39097  sge0fodjrnlem  39133  sge0iun  39136  sge0isum  39144  sge0seq  39163  meadjun  39179  meadjiunlem  39182  meadjiun  39183  ismeannd  39184  psmeasurelem  39187  omeiunle  39231  ovn02  39282  smfpimioo  39496  smfresal  39497  aacllem  42339  amgmwlem  42340  amgmlemALT  42341
  Copyright terms: Public domain W3C validator