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

Theorem ffun 5391
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 5389 . 2  |-  ( F : A --> B  ->  F  Fn  A )
2 fnfun 5341 . 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 5249    Fn wfn 5250   -->wf 5251
This theorem is referenced by:  funssxp  5402  f00  5426  fofun  5452  fun11iun  5493  fimacnv  5657  dff3  5673  fmptco  5691  fliftf  5814  smores2  6371  pmfun  6790  pmresg  6795  fodomr  7012  ac6sfi  7101  fissuni  7160  fipreima  7161  ordtypelem8  7240  ordtypelem9  7241  ordtypelem10  7242  unxpwdom2  7302  cnfcomlem  7402  tcrank  7554  fseqenlem2  7652  carduniima  7723  infmap2  7844  hsmexlem4  8055  hsmexlem5  8056  axdc3lem2  8077  axdc3lem4  8079  smobeth  8208  fpwwe2lem13  8264  fpwwe2  8265  inar1  8397  grur1  8442  nqerid  8557  nn0supp  10017  zexALT  10042  hashkf  11339  hashgval  11340  revco  11489  ccatco  11490  climdm  12028  isercolllem2  12139  isercolllem3  12140  isercoll  12141  sum0  12194  sumz  12195  fsumsers  12201  isumclim  12220  znnen  12491  mrcuni  13523  isacs2  13555  isacs5  14275  cntzmhm2  14815  frgpupval  15083  dprdss  15264  dprd2dlem1  15276  dprd2da  15277  dmdprdsplit2lem  15280  lmhmpreima  15805  lmhmlsp  15806  cygznlem2  16522  iscnp3  16974  subbascn  16984  cnpnei  16993  cnclima  16997  iscncl  16998  cnclsi  17001  cncls  17003  cncnp  17009  cnrest  17013  cnrest2  17014  paste  17022  cnhaus  17082  conima  17151  1stcfb  17171  1stccnp  17188  1stckgenlem  17248  kgencn3  17253  txcnpi  17302  txcnp  17314  xkopt  17349  xkoco2cn  17352  xkococnlem  17353  hmeores  17462  fbasrn  17579  uzrest  17592  rnelfmlem  17647  rnelfm  17648  fmfnfmlem2  17650  fmfnfmlem3  17651  fmfnfmlem4  17652  fmfnfm  17653  cnflf2  17698  lmflf  17700  txflf  17701  clssubg  17791  ghmcnp  17797  metcnp  18087  isngp2  18119  qtopbaslem  18267  tgqioo  18306  re2ndc  18307  bndth  18456  pi1xfrval  18552  pi1coval  18558  tchcph  18667  iscfil2  18692  ovolficcss  18829  volf  18888  volsup  18913  uniioombllem3a  18939  uniioombllem4  18941  uniioombllem5  18942  dyadmbllem  18954  dyadmbl  18955  opnmbllem  18956  opnmblALT  18958  mbfimaicc  18988  ismbfd  18995  ismbf3d  19009  mbfimaopnlem  19010  mbfimaopn2  19012  i1fima  19033  i1fima2  19034  i1fd  19036  itg1addlem4  19054  ellimc2  19227  ellimc3  19229  dvres3  19263  dvres3a  19264  dvidlem  19265  dvcnp  19268  dvadd  19289  dvmul  19290  dvaddf  19291  dvmulf  19292  dvco  19296  dvcof  19297  dvcjbr  19298  dvcj  19299  dvrec  19304  dvcnvlem  19323  dvcnv  19324  dvef  19327  dvferm1  19332  dvferm2  19334  c1liplem1  19343  dvcnvrelem1  19364  dvcnvrelem2  19365  ftc1cn  19390  evlseu  19400  mpfind  19428  mdegldg  19452  mdegcl  19455  deg1n0ima  19475  plyco0  19574  plyeq0  19593  plypf1  19594  plyaddlem1  19595  plymullem1  19596  tayl0  19741  ulmdvlem3  19779  ulmdv  19780  pserdv  19805  dvlog  19998  efopn  20005  dchrelbas2  20476  dchrghm  20495  ghsubgolem  21037  sspg  21304  ssps  21306  sspn  21312  htthlem  21497  issh2  21788  hlimuni  21818  hhsscms  21856  occllem  21882  occl  21883  chscllem4  22219  imaelshi  22638  fmptcof2  23229  curry2ima  23247  xrofsup  23255  esumpfinvallem  23442  mbfmfun  23559  imambfm  23567  dstrvprob  23672  dstfrvel  23674  orvclteinc  23676  erdszelem2  23723  erdszelem7  23728  erdszelem8  23729  cvmliftmolem1  23812  cvmliftlem3  23818  cvmliftlem10  23825  cvmliftlem13  23827  cvmliftlem15  23829  cvmlift2lem9  23842  cvmlift3lem6  23855  cvmlift3lem7  23856  eupap1  23900  nofun  24303  svs3  25488  cmptdst  25568  flfnei2  25577  bwt2  25592  lvsovso  25626  supnuf  25629  rdmob  25748  rcmob  25749  idsubidsup  25857  idsubfun  25858  ivthALT  26258  indexdom  26413  cnres2  26483  heibor1lem  26533  grpokerinj  26575  elrfirn  26770  elmapfun  26789  fnwe2lem2  27148  lmhmfgima  27182  frlmup4  27253  fsuppeq  27259  lindff1  27290  lindfrn  27291  cncmpmax  27703
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 5258  df-f 5259
  Copyright terms: Public domain W3C validator