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

Theorem feqmptd 6399
Description: Deduction form of dffn5 6391. (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 6194 . . 3 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
31, 2syl 17 . 2 (𝜑𝐹 Fn 𝐴)
4 dffn5 6391 . 2 (𝐹 Fn 𝐴𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
53, 4sylib 208 1 (𝜑𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1620  cmpt 4869   Fn wfn 6032  wf 6033  cfv 6037
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-sep 4921  ax-nul 4929  ax-pr 5043
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ral 3043  df-rex 3044  df-rab 3047  df-v 3330  df-sbc 3565  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-sn 4310  df-pr 4312  df-op 4316  df-uni 4577  df-br 4793  df-opab 4853  df-mpt 4870  df-id 5162  df-xp 5260  df-rel 5261  df-cnv 5262  df-co 5263  df-dm 5264  df-iota 6000  df-fun 6039  df-fn 6040  df-f 6041  df-fv 6045
This theorem is referenced by:  feqresmpt  6400  cofmpt  6550  fcoconst  6552  ofco  7070  caofinvl  7077  caofcom  7082  caofass  7084  caofdi  7086  caofdir  7087  caonncan  7088  suppssof1  7485  mapxpen  8279  xpmapenlem  8280  cantnfp1  8739  cantnflem1  8747  cnfcom2lem  8759  infxpenc  9002  pwfseqlem5  9648  gruf  9796  ccatco  13752  cnrecnv  14075  lo1o12  14434  rlimclim1  14446  rlimuni  14451  lo1resb  14465  rlimresb  14466  o1resb  14467  rlimcn1  14489  rlimcn1b  14490  rlimo1  14517  o1rlimmul  14519  caucvgr  14576  ackbijnn  14730  bitsf1ocnv  15339  ramcl  15906  pwsplusgval  16323  pwsmulrval  16324  pwsvscafval  16327  setcepi  16910  prf1st  17016  prf2nd  17017  1st2ndprf  17018  curfuncf  17050  curf2ndf  17059  yonedainv  17093  yonffthlem  17094  prdsidlem  17494  pwsco1mhm  17542  pwsco2mhm  17543  frmdup3lem  17575  frmdup3  17576  grpinvcnv  17655  pwsinvg  17700  pwssub  17701  psgnunilem5  18085  efginvrel1  18312  frgpup3lem  18361  frgpup3  18362  gsumval3  18479  gsumcllem  18480  gsumzf1o  18484  gsumzsplit  18498  gsumconst  18505  gsumzmhm  18508  gsumsub  18519  gsum2dlem2  18541  gsumcom2  18545  dprdfadd  18590  dprdfsub  18591  dprdfeq0  18592  dprdf11  18593  dmdprdsplitlem  18607  dprddisj2  18609  dpjidcl  18628  ablfaclem2  18656  ablfac2  18659  mptscmfsuppd  19102  lmhmvsca  19218  rrgsupp  19464  psrbagaddcl  19543  gsumbagdiaglem  19548  psrass1lem  19550  psrlinv  19570  psrass1  19578  psrcom  19582  mplsubrglem  19612  mplmonmul  19637  mplcoe1  19638  mplcoe5  19641  evlslem2  19685  evlslem6  19686  evlslem1  19688  coe1fval3  19751  coe1sclmul  19825  coe1sclmul2  19827  mulgrhm2  20020  cygznlem2a  20089  frgpcyg  20095  uvcresum  20305  frlmup1  20310  grpvrinv  20375  mhmvlin  20376  mdetleib2  20567  mdetralt  20587  mdetunilem9  20599  cayleyhamilton1  20870  neiptopnei  21109  dfac14  21594  ptcnp  21598  lmcn2  21625  cnmpt11f  21640  cnmpt21f  21648  cnmpt2k  21664  qtopeu  21692  xkocnv  21790  xkohmeo  21791  flfcnp2  21983  istgp2  22067  tmdgsum  22071  symgtgp  22077  subgtgp  22081  tgpconncomp  22088  prdstgpd  22100  tsmsmhm  22121  tsmssub  22124  tgptsmscls  22125  tsmssplit  22127  tsmsxplem1  22128  tlmtgp  22171  ustuqtop  22222  prdsmslem1  22504  prdsxmslem1  22505  prdsxmslem2  22506  tngnm  22627  nmoeq0  22712  cnfldnm  22754  cncfmpt1f  22888  negfcncf  22894  cnrehmeo  22924  evth  22930  evth2  22931  copco  22989  pcopt  22993  pcopt2  22994  pcoass  22995  pcorev2  22999  pi1xfrcnv  23028  ovolctb  23429  ovolfs2  23510  uniioombllem2  23522  uniioombllem3  23524  ismbf  23567  mbfconst  23572  ismbfcn2  23576  mbfmulc2re  23585  mbfadd  23598  mbfsub  23599  mbflimsup  23603  itg1climres  23651  mbfi1flimlem  23659  mbfi1flim  23660  mbfmul  23663  itg2uba  23680  itg2mulclem  23683  itg2mulc  23684  itg2splitlem  23685  itg2monolem1  23687  itg2i1fseq  23692  itg2gt0  23697  itg2cnlem1  23698  itg2cnlem2  23699  i1fibl  23744  itgitg1  23745  iblabslem  23764  iblabs  23765  bddmulibl  23775  cnplimc  23821  limccnp  23825  limccnp2  23826  dvcnp2  23853  dvmulf  23876  dvcmulf  23878  dvcobr  23879  dvcof  23881  dvcjbr  23882  dvcj  23883  dvfre  23884  dvmptcj  23901  dvcnvlem  23909  dvcnv  23910  dvef  23913  dvsincos  23914  rolle  23923  cmvth  23924  dvlip  23926  dvlipcn  23927  dv11cn  23934  dvivthlem1  23941  dvivth  23943  lhop2  23948  dvfsumrlim2  23965  ftc1lem1  23968  ftc1lem2  23969  ftc1a  23970  ftc1lem4  23972  ftc2  23977  ftc2ditglem  23978  ftc2ditg  23979  tdeglem4  23990  tdeglem2  23991  mdegle0  24007  mdegmullem  24008  plypf1  24138  plyco  24167  dgrcolem1  24199  dgrcolem2  24200  dgrco  24201  plycjlem  24202  dvply2g  24210  plydiveu  24223  elqaalem3  24246  taylthlem1  24297  taylthlem2  24298  ulmshft  24314  ulmdvlem1  24324  mtest  24328  mtestbdd  24329  mbfulm  24330  iblulm  24331  itgulm  24332  pserulm  24346  pserdv  24353  abelthlem1  24355  abelthlem3  24357  pige3  24439  eff1olem  24464  logcn  24563  advlog  24570  advlogexp  24571  logtayl  24576  logccv  24579  dvcxp1  24651  dvcxp2  24652  dvcncxp1  24654  resqrtcn  24660  sqrtcn  24661  loglesqrt  24669  dvatan  24832  leibpi  24839  divsqrtsumo1  24880  jensenlem2  24884  amgmlem  24886  lgamgulmlem2  24926  lgamcvg2  24951  ftalem7  24975  basellem9  24985  muinv  25089  dchrmulid2  25147  dchrinvcl  25148  lgseisenlem4  25273  dchrisum0lem2a  25376  logdivsum  25392  mulog2sumlem1  25393  log2sumbnd  25403  hilnormi  28300  chscllem4  28779  hmopidmchi  29290  rabfodom  29622  ofoprabco  29744  fpwrelmapffslem  29787  fpwrelmap  29788  qqhre  30344  prodindf  30365  esumpcvgval  30420  ofcfval4  30447  omssubadd  30642  carsggect  30660  plymulx0  30904  fdvneggt  30958  fdvnegge  30960  itgexpif  30964  ptpconn  31493  cvmliftlem6  31550  cvmliftlem8  31552  cvmlift2lem7  31569  cvmliftphtlem  31577  cvmlift3lem5  31583  elmsubrn  31703  knoppcnlem9  32768  curunc  33673  poimir  33724  broucube  33725  mblfinlem2  33729  volsupnfl  33736  cnambfre  33740  dvtan  33742  itg2addnclem  33743  itg2addnclem2  33744  itg2addnclem3  33745  itg2addnc  33746  itg2gt0cn  33747  itgaddnc  33752  itgmulc2nc  33760  bddiblnc  33762  ftc1cnnclem  33765  ftc1anclem1  33767  ftc1anclem2  33768  ftc1anclem3  33769  ftc1anclem4  33770  ftc1anclem5  33771  ftc1anclem6  33772  ftc1anclem7  33773  ftc1anclem8  33774  ftc1anc  33775  ftc2nc  33776  upixp  33806  mzpsubst  37782  diophun  37808  mendlmod  38234  mendassa  38235  fsovcnvlem  38778  binomcxplemnotnn0  39026  rnsnf  39838  cncfmptss  40291  climliminflimsupd  40505  mulcncff  40553  subcncff  40565  cncfcompt  40568  addcncff  40569  divcncff  40576  cncfiooicclem1  40578  dvsinexp  40597  dvsubf  40600  dvdivf  40609  dvcosax  40613  dvnmul  40630  dvnprodlem1  40633  dvnprodlem2  40634  itgsinexplem1  40641  itgsubsticclem  40663  iblcncfioo  40666  itgiccshift  40668  stoweidlem20  40709  dirkercncflem2  40793  fourierdlem16  40812  fourierdlem21  40817  fourierdlem22  40818  fourierdlem28  40824  fourierdlem39  40835  fourierdlem51  40846  fourierdlem60  40855  fourierdlem61  40856  fourierdlem69  40864  fourierdlem72  40867  fourierdlem73  40868  fourierdlem81  40876  fourierdlem83  40878  fourierdlem84  40879  fourierdlem87  40882  fourierdlem90  40885  fourierdlem93  40888  fourierdlem95  40890  fourierdlem101  40896  fourierdlem103  40898  fourierdlem104  40899  fourierdlem111  40906  etransclem34  40957  etransclem43  40966  etransclem46  40969  sge0tsms  41069  sge0fodjrnlem  41105  sge0iun  41108  sge0isum  41116  sge0seq  41135  meadjun  41151  meadjiunlem  41154  meadjiun  41155  ismeannd  41156  psmeasurelem  41159  omeiunle  41206  ovn02  41257  smfpimioo  41469  smfresal  41470  smfinflem  41498  smflimsuplem3  41503  smfliminflem  41511  aacllem  43029  amgmwlem  43030  amgmlemALT  43031
  Copyright terms: Public domain W3C validator