MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ffun Structured version   Unicode version

Theorem ffun 5566
Description: A mapping is a function. (Contributed by NM, 3-Aug-1994.)
Assertion
Ref Expression
ffun  |-  ( F : A --> B  ->  Fun  F )

Proof of Theorem ffun
StepHypRef Expression
1 ffn 5564 . 2  |-  ( F : A --> B  ->  F  Fn  A )
2 fnfun 5513 . 2  |-  ( F  Fn  A  ->  Fun  F )
31, 2syl 16 1  |-  ( F : A --> B  ->  Fun  F )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   Fun wfun 5417    Fn wfn 5418   -->wf 5419
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-fn 5426  df-f 5427
This theorem is referenced by:  funssxp  5576  f00  5598  fofun  5626  fimacnv  5840  dff3  5861  fmptco  5881  fliftf  6013  fun11iun  6542  frnsuppeq  6707  smores2  6820  pmfun  7237  elmapfun  7241  pmresg  7245  fodomr  7467  ac6sfi  7561  fissuni  7621  fipreima  7622  fdmfifsupp  7635  frnfsuppbi  7653  fsuppmptif  7654  fsuppco2  7657  fsuppcor  7658  ordtypelem8  7744  ordtypelem9  7745  ordtypelem10  7746  unxpwdom2  7808  cantnffvalOLD  7876  cnfcomlem  7937  cnfcomlemOLD  7945  tcrank  8096  fseqenlem2  8200  carduniima  8271  infmap2  8392  hsmexlem4  8603  hsmexlem5  8604  axdc3lem2  8625  axdc3lem4  8627  smobeth  8755  fpwwe2lem13  8814  fpwwe2  8815  inar1  8947  grur1  8992  nqerid  9107  nn0suppOLD  10639  zexALT  10670  hashkf  12110  hashgval  12111  hashfzdm  12207  hashfirdm  12209  revco  12467  ccatco  12468  lswco  12471  climdm  13037  isercolllem2  13148  isercolllem3  13149  isercoll  13150  sum0  13203  sumz  13204  fsumsers  13210  isumclim  13229  znnen  13500  mrcuni  14564  isacs2  14596  isacs5  15347  cntzmhm2  15862  frgpupval  16276  gsumzadd  16414  gsumpt  16459  gsum2dlem2  16467  dprdss  16531  dprd2dlem1  16545  dprd2da  16546  dmdprdsplit2lem  16549  lmhmpreima  17134  lmhmlsp  17135  psrelbasfun  17456  mplvalOLD  17507  mvrcl  17533  ltbwe  17559  evlslem3  17605  evlseu  17607  mpfind  17627  gsumply1subr  17693  cygznlem2  18006  frlmup1  18231  frlmup4  18234  lindff1  18254  lindfrn  18255  iscnp3  18853  subbascn  18863  cnpnei  18873  cnclima  18877  iscncl  18878  cnclsi  18881  cncls  18883  cncnp  18889  cnrest  18894  cnrest2  18895  paste  18903  cnhaus  18963  bwthOLD  19019  conima  19034  1stcfb  19054  1stccnp  19071  1stckgenlem  19131  kgencn3  19136  txcnpi  19186  txcnp  19198  xkopt  19233  xkoco2cn  19236  xkococnlem  19237  hmeores  19349  fbasrn  19462  uzrest  19475  rnelfmlem  19530  rnelfm  19531  fmfnfmlem2  19533  fmfnfmlem3  19534  fmfnfmlem4  19535  fmfnfm  19536  cnflf2  19581  lmflf  19583  txflf  19584  cnextcn  19644  clssubg  19684  ghmcnp  19690  metcnp  20121  metustidOLD  20139  metustid  20140  metustsymOLD  20141  metustsym  20142  metustexhalfOLD  20143  metustexhalf  20144  cfilucfilOLD  20149  cfilucfil  20150  restmetu  20167  isngp2  20194  qtopbaslem  20342  tgqioo  20382  re2ndc  20383  bndth  20535  pi1xfrval  20631  pi1coval  20637  tchcph  20757  iscfil2  20782  rrxcph  20901  ovolficcss  20958  volf  21017  volsup  21042  uniioombllem3a  21069  uniioombllem4  21071  uniioombllem5  21072  dyadmbllem  21084  dyadmbl  21085  opnmbllem  21086  opnmblALT  21088  mbfimaicc  21116  ismbfd  21123  ismbf3d  21137  mbfimaopnlem  21138  mbfimaopn2  21140  i1fima  21161  i1fima2  21162  i1fd  21164  itg1addlem4  21182  ellimc2  21357  ellimc3  21359  dvres3  21393  dvres3a  21394  dvidlem  21395  dvcnp  21398  dvadd  21419  dvmul  21420  dvaddf  21421  dvmulf  21422  dvco  21426  dvcof  21427  dvcjbr  21428  dvcj  21429  dvrec  21434  dvcnvlem  21453  dvcnv  21454  dvef  21457  dvferm1  21462  dvferm2  21464  c1liplem1  21473  dvcnvrelem1  21494  dvcnvrelem2  21495  ftc1cn  21520  mdegldg  21542  mdegcl  21545  deg1n0ima  21565  plyco0  21665  plyeq0  21684  plypf1  21685  plyaddlem1  21686  plymullem1  21687  tayl0  21832  ulmdvlem3  21872  ulmdv  21873  pserdv  21899  dvlog  22101  efopn  22108  dchrelbas2  22581  dchrghm  22600  uhgrafun  23244  eupap1  23602  ghsubgolem  23862  sspg  24131  ssps  24133  sspn  24139  htthlem  24324  issh2  24616  hlimuni  24646  hhsscms  24685  occllem  24711  occl  24712  chscllem4  25048  imaelshi  25467  fmptcof2  25984  curry2ima  26008  fpwrelmapffslem  26037  xrofsup  26060  fsumcvg4  26385  zrhunitpreima  26412  esumpfinvallem  26528  mbfmfun  26674  imambfm  26682  sibfof  26731  sitgclg  26733  eulerpartlemd  26754  eulerpartlemt  26759  eulerpartgbij  26760  eulerpartlemmf  26763  eulerpartlemgvv  26764  eulerpartlemgu  26765  eulerpartlemgf  26767  dstrvprob  26859  dstfrvel  26861  orvclteinc  26863  erdszelem2  27085  erdszelem7  27090  erdszelem8  27091  cvmliftmolem1  27175  cvmliftlem3  27181  cvmliftlem10  27188  cvmliftlem13  27190  cvmliftlem15  27192  cvmlift2lem9  27205  cvmlift3lem6  27218  cvmlift3lem7  27219  ntrivcvgfvn0  27419  ntrivcvgtail  27420  zprodn0  27457  iprodclim  27503  nofun  27795  heicant  28431  opnmbllem0  28432  mblfinlem1  28433  dvtanlem  28446  itg2addnclem  28448  itg2addnclem2  28449  ftc1cnnc  28471  ftc1anclem7  28478  ftc1anc  28480  ftc2nc  28481  ivthALT  28535  indexdom  28633  cnres2  28667  heibor1lem  28713  grpokerinj  28755  elrfirn  29036  fnwe2lem2  29409  lmhmfgima  29442  fsuppeq  29455  arearect  29596  areaquad  29597  cncmpmax  29759  domnmsuppn0  30787  rmsuppss  30788  mndpsuppss  30789  scmsuppss  30790
  Copyright terms: Public domain W3C validator