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

Theorem ffun 5552
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 5550 . 2  |-  ( F : A --> B  ->  F  Fn  A )
2 fnfun 5501 . 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 5407    Fn wfn 5408   -->wf 5409
This theorem is referenced by:  funssxp  5563  f00  5587  fofun  5613  fun11iun  5654  fimacnv  5821  dff3  5841  fmptco  5860  fliftf  5996  smores2  6575  pmfun  6995  pmresg  7000  fodomr  7217  ac6sfi  7310  fissuni  7369  fipreima  7370  ordtypelem8  7450  ordtypelem9  7451  ordtypelem10  7452  unxpwdom2  7512  cnfcomlem  7612  tcrank  7764  fseqenlem2  7862  carduniima  7933  infmap2  8054  hsmexlem4  8265  hsmexlem5  8266  axdc3lem2  8287  axdc3lem4  8289  smobeth  8417  fpwwe2lem13  8473  fpwwe2  8474  inar1  8606  grur1  8651  nqerid  8766  nn0supp  10229  zexALT  10256  hashkf  11575  hashgval  11576  revco  11758  ccatco  11759  climdm  12303  isercolllem2  12414  isercolllem3  12415  isercoll  12416  sum0  12470  sumz  12471  fsumsers  12477  isumclim  12496  znnen  12767  mrcuni  13801  isacs2  13833  isacs5  14553  cntzmhm2  15093  frgpupval  15361  dprdss  15542  dprd2dlem1  15554  dprd2da  15555  dmdprdsplit2lem  15558  lmhmpreima  16079  lmhmlsp  16080  cygznlem2  16804  iscnp3  17262  subbascn  17272  cnpnei  17282  cnclima  17286  iscncl  17287  cnclsi  17290  cncls  17292  cncnp  17298  cnrest  17303  cnrest2  17304  paste  17312  cnhaus  17372  conima  17441  1stcfb  17461  1stccnp  17478  1stckgenlem  17538  kgencn3  17543  txcnpi  17593  txcnp  17605  xkopt  17640  xkoco2cn  17643  xkococnlem  17644  hmeores  17756  fbasrn  17869  uzrest  17882  rnelfmlem  17937  rnelfm  17938  fmfnfmlem2  17940  fmfnfmlem3  17941  fmfnfmlem4  17942  fmfnfm  17943  cnflf2  17988  lmflf  17990  txflf  17991  cnextcn  18051  clssubg  18091  ghmcnp  18097  metcnp  18524  metustidOLD  18542  metustid  18543  metustsymOLD  18544  metustsym  18545  metustexhalfOLD  18546  metustexhalf  18547  cfilucfilOLD  18552  cfilucfil  18553  restmetu  18570  isngp2  18597  qtopbaslem  18745  tgqioo  18784  re2ndc  18785  bndth  18936  pi1xfrval  19032  pi1coval  19038  tchcph  19147  iscfil2  19172  ovolficcss  19319  volf  19378  volsup  19403  uniioombllem3a  19429  uniioombllem4  19431  uniioombllem5  19432  dyadmbllem  19444  dyadmbl  19445  opnmbllem  19446  opnmblALT  19448  mbfimaicc  19478  ismbfd  19485  ismbf3d  19499  mbfimaopnlem  19500  mbfimaopn2  19502  i1fima  19523  i1fima2  19524  i1fd  19526  itg1addlem4  19544  ellimc2  19717  ellimc3  19719  dvres3  19753  dvres3a  19754  dvidlem  19755  dvcnp  19758  dvadd  19779  dvmul  19780  dvaddf  19781  dvmulf  19782  dvco  19786  dvcof  19787  dvcjbr  19788  dvcj  19789  dvrec  19794  dvcnvlem  19813  dvcnv  19814  dvef  19817  dvferm1  19822  dvferm2  19824  c1liplem1  19833  dvcnvrelem1  19854  dvcnvrelem2  19855  ftc1cn  19880  evlseu  19890  mpfind  19918  mdegldg  19942  mdegcl  19945  deg1n0ima  19965  plyco0  20064  plyeq0  20083  plypf1  20084  plyaddlem1  20085  plymullem1  20086  tayl0  20231  ulmdvlem3  20271  ulmdv  20272  pserdv  20298  dvlog  20495  efopn  20502  dchrelbas2  20974  dchrghm  20993  uhgrafun  21293  eupap1  21651  ghsubgolem  21911  sspg  22180  ssps  22182  sspn  22188  htthlem  22373  issh2  22664  hlimuni  22694  hhsscms  22732  occllem  22758  occl  22759  chscllem4  23095  imaelshi  23514  fmptcof2  24029  curry2ima  24050  xrofsup  24079  zrhunitpreima  24315  esumpfinvallem  24417  mbfmfun  24557  imambfm  24565  sibfof  24607  sitgclg  24609  dstrvprob  24682  dstfrvel  24684  orvclteinc  24686  erdszelem2  24831  erdszelem7  24836  erdszelem8  24837  cvmliftmolem1  24921  cvmliftlem3  24927  cvmliftlem10  24934  cvmliftlem13  24936  cvmliftlem15  24938  cvmlift2lem9  24951  cvmlift3lem6  24964  cvmlift3lem7  24965  ntrivcvgfvn0  25180  ntrivcvgtail  25181  zprodn0  25218  iprodclim  25264  nofun  25517  mblfinlem  26143  itg2addnclem  26155  itg2addnclem2  26156  ftc1cnnc  26178  ivthALT  26228  indexdom  26326  cnres2  26362  heibor1lem  26408  grpokerinj  26450  elrfirn  26639  elmapfun  26658  fnwe2lem2  27016  lmhmfgima  27050  frlmup4  27121  fsuppeq  27127  lindff1  27158  lindfrn  27159  cncmpmax  27570  hashfirdm  27996  hashfzdm  27997
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 178  df-an 361  df-fn 5416  df-f 5417
  Copyright terms: Public domain W3C validator