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

Theorem ffun 5731
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 5729 . 2  |-  ( F : A --> B  ->  F  Fn  A )
2 fnfun 5676 . 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 5580    Fn wfn 5581   -->wf 5582
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 5589  df-f 5590
This theorem is referenced by:  funssxp  5742  f00  5765  fofun  5794  fimacnv  6011  dff3  6032  fmptco  6052  fliftf  6199  fun11iun  6741  frnsuppeq  6910  smores2  7022  pmfun  7435  elmapfun  7439  pmresg  7443  fodomr  7665  ac6sfi  7760  fissuni  7821  fipreima  7822  fdmfifsupp  7835  frnfsuppbi  7854  fsuppmptif  7855  fsuppco2  7858  fsuppcor  7859  ordtypelem8  7946  ordtypelem9  7947  ordtypelem10  7948  unxpwdom2  8010  cantnffvalOLD  8078  cnfcomlem  8139  cnfcomlemOLD  8147  tcrank  8298  fseqenlem2  8402  carduniima  8473  infmap2  8594  hsmexlem4  8805  hsmexlem5  8806  axdc3lem2  8827  axdc3lem4  8829  smobeth  8957  fpwwe2lem13  9016  fpwwe2  9017  inar1  9149  grur1  9194  nqerid  9307  nn0suppOLD  10846  zexALT  10879  hashkf  12371  hashgval  12372  hashfzdm  12460  hashfirdm  12462  revco  12759  ccatco  12760  lswco  12763  climdm  13336  isercolllem2  13447  isercolllem3  13448  isercoll  13449  sum0  13502  sumz  13503  fsumsers  13509  isumclim  13531  znnen  13803  mrcuni  14872  isacs2  14904  isacs5  15655  cntzmhm2  16172  frgpupval  16588  gsumzadd  16726  gsumpt  16779  gsum2dlem2  16789  dprdss  16866  dprd2dlem1  16880  dprd2da  16881  dmdprdsplit2lem  16884  lmhmpreima  17477  lmhmlsp  17478  psrelbasfun  17804  mplvalOLD  17856  mvrcl  17882  ltbwe  17908  evlslem3  17954  evlseu  17956  mpfind  17976  gsumply1subr  18046  cygznlem2  18374  frlmup1  18599  frlmup4  18602  lindff1  18622  lindfrn  18623  iscnp3  19511  subbascn  19521  cnpnei  19531  cnclima  19535  iscncl  19536  cnclsi  19539  cncls  19541  cncnp  19547  cnrest  19552  cnrest2  19553  paste  19561  cnhaus  19621  bwthOLD  19677  conima  19692  1stcfb  19712  1stccnp  19729  1stckgenlem  19789  kgencn3  19794  txcnpi  19844  txcnp  19856  xkopt  19891  xkoco2cn  19894  xkococnlem  19895  hmeores  20007  fbasrn  20120  uzrest  20133  rnelfmlem  20188  rnelfm  20189  fmfnfmlem2  20191  fmfnfmlem3  20192  fmfnfmlem4  20193  fmfnfm  20194  cnflf2  20239  lmflf  20241  txflf  20242  cnextcn  20302  clssubg  20342  ghmcnp  20348  metcnp  20779  metustidOLD  20797  metustid  20798  metustsymOLD  20799  metustsym  20800  metustexhalfOLD  20801  metustexhalf  20802  cfilucfilOLD  20807  cfilucfil  20808  restmetu  20825  isngp2  20852  qtopbaslem  21000  tgqioo  21040  re2ndc  21041  bndth  21193  pi1xfrval  21289  pi1coval  21295  tchcph  21415  iscfil2  21440  rrxcph  21559  ovolficcss  21616  volf  21675  volsup  21701  uniioombllem3a  21728  uniioombllem4  21730  uniioombllem5  21731  dyadmbllem  21743  dyadmbl  21744  opnmbllem  21745  opnmblALT  21747  mbfimaicc  21775  ismbfd  21782  ismbf3d  21796  mbfimaopnlem  21797  mbfimaopn2  21799  i1fima  21820  i1fima2  21821  i1fd  21823  itg1addlem4  21841  ellimc2  22016  ellimc3  22018  dvres3  22052  dvres3a  22053  dvidlem  22054  dvcnp  22057  dvadd  22078  dvmul  22079  dvaddf  22080  dvmulf  22081  dvco  22085  dvcof  22086  dvcjbr  22087  dvcj  22088  dvrec  22093  dvcnvlem  22112  dvcnv  22113  dvef  22116  dvferm1  22121  dvferm2  22123  c1liplem1  22132  dvcnvrelem1  22153  dvcnvrelem2  22154  ftc1cn  22179  mdegldg  22201  mdegcl  22204  deg1n0ima  22224  plyco0  22324  plyeq0  22343  plypf1  22344  plyaddlem1  22345  plymullem1  22346  tayl0  22491  ulmdvlem3  22531  ulmdv  22532  pserdv  22558  dvlog  22760  efopn  22767  dchrelbas2  23240  dchrghm  23259  uhgrafun  23976  eupap1  24652  ghsubgolem  25048  sspg  25317  ssps  25319  sspn  25325  htthlem  25510  issh2  25802  hlimuni  25832  hhsscms  25871  occllem  25897  occl  25898  chscllem4  26234  imaelshi  26653  fmptcof2  27174  curry2ima  27198  fpwrelmapffslem  27227  xrofsup  27250  xrge0tsmsd  27438  fsumcvg4  27568  zrhunitpreima  27595  esumpfinvallem  27720  mbfmfun  27865  imambfm  27873  sibfof  27922  sitgclg  27924  eulerpartlemd  27945  eulerpartlemt  27950  eulerpartgbij  27951  eulerpartlemmf  27954  eulerpartlemgvv  27955  eulerpartlemgu  27956  eulerpartlemgf  27958  dstrvprob  28050  dstfrvel  28052  orvclteinc  28054  erdszelem2  28276  erdszelem7  28281  erdszelem8  28282  cvmliftmolem1  28366  cvmliftlem3  28372  cvmliftlem10  28379  cvmliftlem13  28381  cvmliftlem15  28383  cvmlift2lem9  28396  cvmlift3lem6  28409  cvmlift3lem7  28410  ntrivcvgfvn0  28610  ntrivcvgtail  28611  zprodn0  28648  iprodclim  28694  nofun  28986  heicant  29626  opnmbllem0  29627  mblfinlem1  29628  dvtanlem  29641  itg2addnclem  29643  itg2addnclem2  29644  ftc1cnnc  29666  ftc1anclem7  29673  ftc1anc  29675  ftc2nc  29676  ivthALT  29730  indexdom  29828  cnres2  29862  heibor1lem  29908  grpokerinj  29950  elrfirn  30231  fnwe2lem2  30601  lmhmfgima  30634  fsuppeq  30647  arearect  30788  areaquad  30789  cncmpmax  30985  evthiccabs  31093  limccog  31162  cncficcgt0  31227  dvsinax  31241  fperdvper  31248  ditgeqiooicc  31278  dirkercncflem2  31404  fourierdlem20  31427  fourierdlem42  31449  fourierdlem63  31470  fourierdlem76  31483  fourierdlem82  31489  fourierdlem93  31500  fourierdlem97  31504  fourierdlem113  31520  domnmsuppn0  32035  rmsuppss  32036  mndpsuppss  32037  scmsuppss  32038
  Copyright terms: Public domain W3C validator