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

Theorem ffun 5595
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 5593 . 2  |-  ( F : A --> B  ->  F  Fn  A )
2 fnfun 5544 . 2  |-  ( F  Fn  A  ->  Fun  F )
31, 2syl 16 1  |-  ( F : A --> B  ->  Fun  F )
Colors of variables: wff set class
Syntax hints:    -> wi 4   Fun wfun 5450    Fn wfn 5451   -->wf 5452
This theorem is referenced by:  funssxp  5606  f00  5630  fofun  5656  fun11iun  5697  fimacnv  5864  dff3  5884  fmptco  5903  fliftf  6039  smores2  6618  pmfun  7038  pmresg  7043  fodomr  7260  ac6sfi  7353  fissuni  7413  fipreima  7414  ordtypelem8  7496  ordtypelem9  7497  ordtypelem10  7498  unxpwdom2  7558  cnfcomlem  7658  tcrank  7810  fseqenlem2  7908  carduniima  7979  infmap2  8100  hsmexlem4  8311  hsmexlem5  8312  axdc3lem2  8333  axdc3lem4  8335  smobeth  8463  fpwwe2lem13  8519  fpwwe2  8520  inar1  8652  grur1  8697  nqerid  8812  nn0supp  10275  zexALT  10302  hashkf  11622  hashgval  11623  revco  11805  ccatco  11806  climdm  12350  isercolllem2  12461  isercolllem3  12462  isercoll  12463  sum0  12517  sumz  12518  fsumsers  12524  isumclim  12543  znnen  12814  mrcuni  13848  isacs2  13880  isacs5  14600  cntzmhm2  15140  frgpupval  15408  dprdss  15589  dprd2dlem1  15601  dprd2da  15602  dmdprdsplit2lem  15605  lmhmpreima  16126  lmhmlsp  16127  cygznlem2  16851  iscnp3  17310  subbascn  17320  cnpnei  17330  cnclima  17334  iscncl  17335  cnclsi  17338  cncls  17340  cncnp  17346  cnrest  17351  cnrest2  17352  paste  17360  cnhaus  17420  bwth  17475  conima  17490  1stcfb  17510  1stccnp  17527  1stckgenlem  17587  kgencn3  17592  txcnpi  17642  txcnp  17654  xkopt  17689  xkoco2cn  17692  xkococnlem  17693  hmeores  17805  fbasrn  17918  uzrest  17931  rnelfmlem  17986  rnelfm  17987  fmfnfmlem2  17989  fmfnfmlem3  17990  fmfnfmlem4  17991  fmfnfm  17992  cnflf2  18037  lmflf  18039  txflf  18040  cnextcn  18100  clssubg  18140  ghmcnp  18146  metcnp  18573  metustidOLD  18591  metustid  18592  metustsymOLD  18593  metustsym  18594  metustexhalfOLD  18595  metustexhalf  18596  cfilucfilOLD  18601  cfilucfil  18602  restmetu  18619  isngp2  18646  qtopbaslem  18794  tgqioo  18833  re2ndc  18834  bndth  18985  pi1xfrval  19081  pi1coval  19087  tchcph  19196  iscfil2  19221  ovolficcss  19368  volf  19427  volsup  19452  uniioombllem3a  19478  uniioombllem4  19480  uniioombllem5  19481  dyadmbllem  19493  dyadmbl  19494  opnmbllem  19495  opnmblALT  19497  mbfimaicc  19527  ismbfd  19534  ismbf3d  19548  mbfimaopnlem  19549  mbfimaopn2  19551  i1fima  19572  i1fima2  19573  i1fd  19575  itg1addlem4  19593  ellimc2  19766  ellimc3  19768  dvres3  19802  dvres3a  19803  dvidlem  19804  dvcnp  19807  dvadd  19828  dvmul  19829  dvaddf  19830  dvmulf  19831  dvco  19835  dvcof  19836  dvcjbr  19837  dvcj  19838  dvrec  19843  dvcnvlem  19862  dvcnv  19863  dvef  19866  dvferm1  19871  dvferm2  19873  c1liplem1  19882  dvcnvrelem1  19903  dvcnvrelem2  19904  ftc1cn  19929  evlseu  19939  mpfind  19967  mdegldg  19991  mdegcl  19994  deg1n0ima  20014  plyco0  20113  plyeq0  20132  plypf1  20133  plyaddlem1  20134  plymullem1  20135  tayl0  20280  ulmdvlem3  20320  ulmdv  20321  pserdv  20347  dvlog  20544  efopn  20551  dchrelbas2  21023  dchrghm  21042  uhgrafun  21342  eupap1  21700  ghsubgolem  21960  sspg  22229  ssps  22231  sspn  22237  htthlem  22422  issh2  22713  hlimuni  22743  hhsscms  22781  occllem  22807  occl  22808  chscllem4  23144  imaelshi  23563  fmptcof2  24078  curry2ima  24099  xrofsup  24128  zrhunitpreima  24364  esumpfinvallem  24466  mbfmfun  24606  imambfm  24614  sibfof  24656  sitgclg  24658  dstrvprob  24731  dstfrvel  24733  orvclteinc  24735  erdszelem2  24880  erdszelem7  24885  erdszelem8  24886  cvmliftmolem1  24970  cvmliftlem3  24976  cvmliftlem10  24983  cvmliftlem13  24985  cvmliftlem15  24987  cvmlift2lem9  25000  cvmlift3lem6  25013  cvmlift3lem7  25014  ntrivcvgfvn0  25229  ntrivcvgtail  25230  zprodn0  25267  iprodclim  25313  nofun  25606  opnmbllem0  26244  mblfinlem1  26245  itg2addnclem  26258  itg2addnclem2  26259  ftc1cnnc  26281  ftc1anclem7  26288  ftc1anc  26290  ftc2nc  26291  ivthALT  26340  indexdom  26438  cnres2  26474  heibor1lem  26520  grpokerinj  26562  elrfirn  26751  elmapfun  26770  fnwe2lem2  27128  lmhmfgima  27161  frlmup4  27232  fsuppeq  27238  lindff1  27269  lindfrn  27270  cncmpmax  27681  hashfirdm  28176  hashfzdm  28177
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 179  df-an 362  df-fn 5459  df-f 5460
  Copyright terms: Public domain W3C validator