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

Theorem feqmptd 6715
Description: Deduction form of dffn5 6706. (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 6495 . 2 (𝜑𝐹 Fn 𝐴)
3 dffn5 6706 . 2 (𝐹 Fn 𝐴𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
42, 3sylib 221 1 (𝜑𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  cmpt 5122   Fn wfn 6329  wf 6330  cfv 6334
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pr 5307
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ral 3135  df-rex 3136  df-v 3471  df-sbc 3748  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-br 5043  df-opab 5105  df-mpt 5123  df-id 5437  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-fv 6342
This theorem is referenced by:  feqresmpt  6716  cofmpt  6876  fcoconst  6878  ofco  7414  caofinvl  7421  caofcom  7426  caofass  7428  caofdi  7430  caofdir  7431  caonncan  7432  suppssof1  7850  mapxpen  8671  xpmapenlem  8672  cantnfp1  9132  cantnflem1  9140  cnfcom2lem  9152  infxpenc  9433  pwfseqlem5  10074  gruf  10222  ccatco  14188  cnrecnv  14515  rlimclim1  14893  rlimuni  14898  lo1resb  14912  rlimresb  14913  o1resb  14914  rlimcn1  14936  rlimo1  14964  o1rlimmul  14966  caucvgr  15023  ackbijnn  15174  bitsf1ocnv  15782  ramcl  16354  pwsplusgval  16754  pwsmulrval  16755  pwsvscafval  16758  setcepi  17339  prf1st  17445  prf2nd  17446  1st2ndprf  17447  curfuncf  17479  curf2ndf  17488  yonedainv  17522  yonffthlem  17523  prdsidlem  17934  pwsco1mhm  17987  pwsco2mhm  17988  frmdup3lem  18022  frmdup3  18023  grpinvcnv  18158  pwsinvg  18203  pwssub  18204  efginvrel1  18845  frgpup3lem  18894  frgpup3  18895  gsumval3  19018  gsumcllem  19019  gsumzf1o  19023  gsumzsplit  19038  gsumconst  19045  gsumzmhm  19048  gsumsub  19059  gsum2dlem2  19082  gsumcom2  19086  dprdfadd  19133  dprdfsub  19134  dprdfeq0  19135  dprdf11  19136  dmdprdsplitlem  19150  dprddisj2  19152  dpjidcl  19171  ablfaclem2  19199  ablfac2  19202  mptscmfsuppd  19691  lmhmvsca  19808  rrgsupp  20055  mulgrhm2  20190  cygznlem2a  20257  frgpcyg  20263  uvcresum  20480  frlmup1  20485  psrbagaddcl  20606  gsumbagdiaglem  20611  psrass1lem  20613  psrlinv  20633  psrass1  20641  psrcom  20645  mplsubrglem  20675  mplmonmul  20702  mplcoe1  20703  mplcoe5  20706  evlslem2  20749  evlslem6  20751  evlslem1  20752  coe1fval3  20835  coe1sclmul  20909  coe1sclmul2  20911  grpvrinv  21001  mhmvlin  21002  mdetleib2  21191  mdetunilem9  21223  cayleyhamilton1  21495  neiptopnei  21735  dfac14  22221  ptcnp  22225  lmcn2  22252  cnmpt11f  22267  cnmpt21f  22275  cnmpt2k  22291  qtopeu  22319  xkocnv  22417  xkohmeo  22418  flfcnp2  22610  istgp2  22694  tmdgsum  22698  subgtgp  22708  symgtgp  22709  tgpconncomp  22716  prdstgpd  22728  tsmssub  22752  tgptsmscls  22753  tsmssplit  22755  tsmsxplem1  22756  tlmtgp  22799  ustuqtop  22850  prdsmslem1  23132  prdsxmslem1  23133  prdsxmslem2  23134  tngnm  23255  nmoeq0  23340  cnfldnm  23382  cncfmpt1f  23517  negfcncf  23526  cnrehmeo  23556  evth  23562  evth2  23563  copco  23621  pcopt  23625  pcopt2  23626  pcoass  23627  pcorev2  23631  pi1xfrcnv  23660  ovolctb  24092  ovolfs2  24173  uniioombllem2  24185  ismbf  24230  mbfconst  24235  mbfmulc2re  24250  mbfadd  24263  mbfsub  24264  mbflimsup  24268  mbfi1flimlem  24324  mbfi1flim  24325  mbfmul  24328  itg2uba  24345  itg2mulclem  24348  itg2mulc  24349  itg2splitlem  24350  itg2monolem1  24352  itg2i1fseq  24357  itg2gt0  24362  itg2cnlem1  24363  itg2cnlem2  24364  i1fibl  24409  itgitg1  24410  bddmulibl  24440  bddiblnc  24443  cnplimc  24488  limccnp2  24493  dvcnp2  24521  dvmulf  24544  dvcmulf  24546  dvcobr  24547  dvcof  24549  dvcj  24551  dvfre  24552  dvmptcj  24569  dvcnvlem  24577  dvcnv  24578  dvef  24581  dvsincos  24582  rolle  24591  cmvth  24592  dvlip  24594  dvlipcn  24595  dv11cn  24602  dvivthlem1  24609  dvivth  24611  lhop2  24616  dvfsumrlim2  24633  ftc1lem1  24636  ftc1lem2  24637  ftc1a  24638  ftc1lem4  24640  ftc2  24645  ftc2ditglem  24646  ftc2ditg  24647  tdeglem4  24659  tdeglem2  24660  mdegle0  24676  mdegmullem  24677  plypf1  24807  plyco  24836  dgrcolem1  24868  dgrcolem2  24869  dgrco  24870  plycjlem  24871  dvply2g  24879  plydiveu  24892  elqaalem3  24915  taylthlem1  24966  taylthlem2  24967  ulmshft  24983  ulmdvlem1  24993  mtest  24997  mtestbdd  24998  mbfulm  24999  iblulm  25000  itgulm  25001  pserulm  25015  pserdv  25022  abelthlem1  25024  abelthlem3  25026  pige3ALT  25110  eff1olem  25138  logcn  25236  advlog  25243  advlogexp  25244  logtayl  25249  logccv  25252  dvcxp1  25327  dvcxp2  25328  dvcncxp1  25330  resqrtcn  25336  sqrtcn  25337  loglesqrt  25345  dvatan  25519  leibpi  25526  divsqrtsumo1  25567  jensenlem2  25571  amgmlem  25573  lgamgulmlem2  25613  ftalem7  25662  basellem9  25672  muinv  25776  dchrmulid2  25834  dchrinvcl  25835  dchrisum0lem2a  26099  logdivsum  26115  mulog2sumlem1  26116  log2sumbnd  26126  hilnormi  28944  chscllem4  29421  hmopidmchi  29932  rabfodom  30272  ofoprabco  30417  fpwrelmapffslem  30478  fpwrelmap  30479  lbsdiflsp0  31079  fedgmullem1  31082  qqhre  31335  prodindf  31356  esumpcvgval  31411  ofcfval4  31438  omssubadd  31632  carsggect  31650  plymulx0  31891  fdvneggt  31945  fdvnegge  31947  itgexpif  31951  ptpconn  32554  cvmliftlem6  32611  cvmliftlem8  32613  cvmlift2lem7  32630  cvmliftphtlem  32638  cvmlift3lem5  32644  elmsubrn  32849  knoppcnlem9  33914  curunc  35001  poimir  35052  broucube  35053  mblfinlem2  35057  volsupnfl  35064  cnambfre  35067  dvtan  35069  itg2addnclem  35070  itg2addnclem2  35071  itg2addnclem3  35072  itg2addnc  35073  itg2gt0cn  35074  itgaddnc  35079  itgmulc2nc  35087  ftc1cnnclem  35090  ftc1anclem1  35092  ftc1anclem2  35093  ftc1anclem3  35094  ftc1anclem4  35095  ftc1anclem5  35096  ftc1anclem6  35097  ftc1anclem7  35098  ftc1anclem8  35099  ftc1anc  35100  ftc2nc  35101  upixp  35129  mzpsubst  39623  diophun  39648  mendlmod  40071  mendassa  40072  fsovcnvlem  40649  binomcxplemnotnn0  40998  rnsnf  41752  cncfmptss  42172  climliminflimsupd  42386  mulcncff  42455  subcncff  42465  cncfcompt  42468  addcncff  42469  divcncff  42476  cncfiooicclem1  42478  dvsinexp  42496  dvsubf  42499  dvdivf  42507  dvcosax  42511  dvnmul  42528  dvnprodlem1  42531  dvnprodlem2  42532  itgsinexplem1  42539  itgsubsticclem  42560  iblcncfioo  42563  itgiccshift  42565  stoweidlem20  42605  dirkercncflem2  42689  fourierdlem16  42708  fourierdlem21  42713  fourierdlem22  42714  fourierdlem28  42720  fourierdlem39  42731  fourierdlem51  42742  fourierdlem60  42751  fourierdlem61  42752  fourierdlem69  42760  fourierdlem72  42763  fourierdlem73  42764  fourierdlem81  42772  fourierdlem83  42774  fourierdlem84  42775  fourierdlem87  42778  fourierdlem90  42781  fourierdlem93  42784  fourierdlem95  42786  fourierdlem101  42792  fourierdlem103  42794  fourierdlem104  42795  fourierdlem111  42802  etransclem34  42853  etransclem43  42862  etransclem46  42865  sge0tsms  42962  sge0fodjrnlem  42998  sge0iun  43001  sge0isum  43009  sge0seq  43028  meadjun  43044  meadjiunlem  43047  meadjiun  43048  ismeannd  43049  psmeasurelem  43052  omeiunle  43099  ovn02  43150  smfpimioo  43362  smfresal  43363  smfinflem  43391  smflimsuplem3  43396  smfliminflem  43404  1arymaptfo  45000  aacllem  45272  amgmwlem  45273  amgmlemALT  45274
  Copyright terms: Public domain W3C validator