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

Theorem ffun 5407
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 5405 . 2  |-  ( F : A --> B  ->  F  Fn  A )
2 fnfun 5357 . 2  |-  ( F  Fn  A  ->  Fun  F )
31, 2syl 15 1  |-  ( F : A --> B  ->  Fun  F )
Colors of variables: wff set class
Syntax hints:    -> wi 4   Fun wfun 5265    Fn wfn 5266   -->wf 5267
This theorem is referenced by:  funssxp  5418  f00  5442  fofun  5468  fun11iun  5509  fimacnv  5673  dff3  5689  fmptco  5707  fliftf  5830  smores2  6387  pmfun  6806  pmresg  6811  fodomr  7028  ac6sfi  7117  fissuni  7176  fipreima  7177  ordtypelem8  7256  ordtypelem9  7257  ordtypelem10  7258  unxpwdom2  7318  cnfcomlem  7418  tcrank  7570  fseqenlem2  7668  carduniima  7739  infmap2  7860  hsmexlem4  8071  hsmexlem5  8072  axdc3lem2  8093  axdc3lem4  8095  smobeth  8224  fpwwe2lem13  8280  fpwwe2  8281  inar1  8413  grur1  8458  nqerid  8573  nn0supp  10033  zexALT  10058  hashkf  11355  hashgval  11356  revco  11505  ccatco  11506  climdm  12044  isercolllem2  12155  isercolllem3  12156  isercoll  12157  sum0  12210  sumz  12211  fsumsers  12217  isumclim  12236  znnen  12507  mrcuni  13539  isacs2  13571  isacs5  14291  cntzmhm2  14831  frgpupval  15099  dprdss  15280  dprd2dlem1  15292  dprd2da  15293  dmdprdsplit2lem  15296  lmhmpreima  15821  lmhmlsp  15822  cygznlem2  16538  iscnp3  16990  subbascn  17000  cnpnei  17009  cnclima  17013  iscncl  17014  cnclsi  17017  cncls  17019  cncnp  17025  cnrest  17029  cnrest2  17030  paste  17038  cnhaus  17098  conima  17167  1stcfb  17187  1stccnp  17204  1stckgenlem  17264  kgencn3  17269  txcnpi  17318  txcnp  17330  xkopt  17365  xkoco2cn  17368  xkococnlem  17369  hmeores  17478  fbasrn  17595  uzrest  17608  rnelfmlem  17663  rnelfm  17664  fmfnfmlem2  17666  fmfnfmlem3  17667  fmfnfmlem4  17668  fmfnfm  17669  cnflf2  17714  lmflf  17716  txflf  17717  clssubg  17807  ghmcnp  17813  metcnp  18103  isngp2  18135  qtopbaslem  18283  tgqioo  18322  re2ndc  18323  bndth  18472  pi1xfrval  18568  pi1coval  18574  tchcph  18683  iscfil2  18708  ovolficcss  18845  volf  18904  volsup  18929  uniioombllem3a  18955  uniioombllem4  18957  uniioombllem5  18958  dyadmbllem  18970  dyadmbl  18971  opnmbllem  18972  opnmblALT  18974  mbfimaicc  19004  ismbfd  19011  ismbf3d  19025  mbfimaopnlem  19026  mbfimaopn2  19028  i1fima  19049  i1fima2  19050  i1fd  19052  itg1addlem4  19070  ellimc2  19243  ellimc3  19245  dvres3  19279  dvres3a  19280  dvidlem  19281  dvcnp  19284  dvadd  19305  dvmul  19306  dvaddf  19307  dvmulf  19308  dvco  19312  dvcof  19313  dvcjbr  19314  dvcj  19315  dvrec  19320  dvcnvlem  19339  dvcnv  19340  dvef  19343  dvferm1  19348  dvferm2  19350  c1liplem1  19359  dvcnvrelem1  19380  dvcnvrelem2  19381  ftc1cn  19406  evlseu  19416  mpfind  19444  mdegldg  19468  mdegcl  19471  deg1n0ima  19491  plyco0  19590  plyeq0  19609  plypf1  19610  plyaddlem1  19611  plymullem1  19612  tayl0  19757  ulmdvlem3  19795  ulmdv  19796  pserdv  19821  dvlog  20014  efopn  20021  dchrelbas2  20492  dchrghm  20511  ghsubgolem  21053  sspg  21320  ssps  21322  sspn  21328  htthlem  21513  issh2  21804  hlimuni  21834  hhsscms  21872  occllem  21898  occl  21899  chscllem4  22235  imaelshi  22654  fmptcof2  23244  curry2ima  23262  xrofsup  23270  esumpfinvallem  23457  mbfmfun  23574  imambfm  23582  dstrvprob  23687  dstfrvel  23689  orvclteinc  23691  erdszelem2  23738  erdszelem7  23743  erdszelem8  23744  cvmliftmolem1  23827  cvmliftlem3  23833  cvmliftlem10  23840  cvmliftlem13  23842  cvmliftlem15  23844  cvmlift2lem9  23857  cvmlift3lem6  23870  cvmlift3lem7  23871  eupap1  23915  zprodn0  24162  nofun  24374  itg2addnclem  25003  itg2addnclem2  25004  ftc1cnnc  25025  svs3  25591  cmptdst  25671  flfnei2  25680  bwt2  25695  lvsovso  25729  supnuf  25732  rdmob  25851  rcmob  25852  idsubidsup  25960  idsubfun  25961  ivthALT  26361  indexdom  26516  cnres2  26586  heibor1lem  26636  grpokerinj  26678  elrfirn  26873  elmapfun  26892  fnwe2lem2  27251  lmhmfgima  27285  frlmup4  27356  fsuppeq  27362  lindff1  27393  lindfrn  27394  cncmpmax  27806
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-fn 5274  df-f 5275
  Copyright terms: Public domain W3C validator