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

Theorem ffun 5754
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 5751 . 2  |-  ( F : A --> B  ->  F  Fn  A )
2 fnfun 5695 . 2  |-  ( F  Fn  A  ->  Fun  F )
31, 2syl 17 1  |-  ( F : A --> B  ->  Fun  F )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   Fun wfun 5595    Fn wfn 5596   -->wf 5597
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 190  df-an 377  df-fn 5604  df-f 5605
This theorem is referenced by:  funssxp  5765  f00  5788  fofun  5817  fimacnv  6035  dff3  6058  fmptco  6080  fliftf  6233  fun11iun  6780  frnsuppeq  6953  smores2  7099  pmfun  7517  elmapfun  7521  pmresg  7525  fodomr  7749  ac6sfi  7841  fissuni  7905  fipreima  7906  fdmfifsupp  7919  frnfsuppbi  7938  fsuppmptif  7939  fsuppco2  7942  fsuppcor  7943  ordtypelem8  8066  ordtypelem9  8067  ordtypelem10  8068  unxpwdom2  8129  cnfcomlem  8230  tcrank  8381  fseqenlem2  8482  carduniima  8553  infmap2  8674  hsmexlem4  8885  hsmexlem5  8886  axdc3lem2  8907  axdc3lem4  8909  smobeth  9037  fpwwe2lem13  9093  fpwwe2  9094  inar1  9226  grur1  9271  nqerid  9384  zexALT  10985  hashkf  12549  hashgval  12550  hashfzdm  12645  hashfirdm  12647  revco  12968  ccatco  12969  lswco  12972  climdm  13667  isercolllem2  13778  isercolllem3  13779  isercoll  13780  sum0  13836  sumz  13837  fsumsers  13843  isumclim  13867  ntrivcvgfvn0  14004  ntrivcvgtail  14005  zprodn0  14042  iprodclim  14100  znnen  14314  mrcuni  15576  isacs2  15608  isacs5  16467  cntzmhm2  17042  frgpupval  17473  gsumzadd  17604  gsumpt  17643  gsum2dlem2  17652  dprdss  17711  dprd2dlem1  17723  dprd2da  17724  dmdprdsplit2lem  17727  lmhmpreima  18320  lmhmlsp  18321  psrelbasfun  18653  mvrcl  18722  evlslem3  18786  evlseu  18788  mpfind  18808  gsumply1subr  18876  cygznlem2  19188  frlmup1  19405  frlmup4  19408  lindff1  19427  lindfrn  19428  iscnp3  20309  subbascn  20319  cnpnei  20329  cnclima  20333  iscncl  20334  cnclsi  20337  cncls  20339  cncnp  20345  cnrest2  20351  paste  20359  cnhaus  20419  conima  20489  1stcfb  20509  1stccnp  20526  1stckgenlem  20617  kgencn3  20622  txcnpi  20672  txcnp  20684  xkopt  20719  xkoco2cn  20722  xkococnlem  20723  hmeores  20835  fbasrn  20948  uzrest  20961  rnelfmlem  21016  rnelfm  21017  fmfnfmlem2  21019  fmfnfmlem3  21020  fmfnfmlem4  21021  fmfnfm  21022  cnflf2  21067  lmflf  21069  txflf  21070  cnextcn  21131  clssubg  21172  ghmcnp  21178  metcnp  21605  metustid  21618  metustsym  21619  metustexhalf  21620  cfilucfil  21623  restmetu  21634  isngp2  21660  qtopbaslem  21828  tgqioo  21867  re2ndc  21868  bndth  22035  pi1xfrval  22134  pi1coval  22140  tchcph  22260  iscfil2  22285  rrxcph  22400  ovolficcss  22471  volf  22532  volsup  22558  uniioombllem3a  22591  uniioombllem4  22593  uniioombllem5  22594  dyadmbllem  22606  dyadmbl  22607  opnmbllem  22608  opnmblALT  22610  mbfimaicc  22638  ismbfd  22645  ismbf3d  22659  mbfimaopnlem  22660  mbfimaopn2  22662  i1fima  22685  i1fima2  22686  i1fd  22688  itg1addlem4  22706  ellimc2  22881  ellimc3  22883  dvres3  22917  dvres3a  22918  dvidlem  22919  dvcnp  22922  dvadd  22943  dvmul  22944  dvaddf  22945  dvmulf  22946  dvco  22950  dvcof  22951  dvcjbr  22952  dvcj  22953  dvrec  22958  dvcnvlem  22977  dvcnv  22978  dvef  22981  dvferm1  22986  dvferm2  22988  c1liplem1  22997  dvcnvrelem1  23018  dvcnvrelem2  23019  ftc1cn  23044  mdegldg  23064  mdegcl  23067  deg1n0ima  23087  plyco0  23195  plyeq0  23214  plypf1  23215  plyaddlem1  23216  plymullem1  23217  tayl0  23366  ulmdvlem3  23406  ulmdv  23407  pserdv  23433  dvlog  23645  efopn  23652  relogbf  23777  dchrelbas2  24214  dchrghm  24233  uhgrafun  25076  eupap1  25753  ghsubgolemOLD  26147  sspg  26416  ssps  26418  sspn  26424  htthlem  26619  issh2  26911  hlimuni  26940  hhsscms  26979  occllem  27005  occl  27006  chscllem4  27342  imaelshi  27760  fmptcof2  28308  curry2ima  28338  fpwrelmapffslem  28366  xrofsup  28402  xrge0tsmsd  28597  smatrcl  28671  mdetpmtr1  28698  locfinreflem  28716  fsumcvg4  28805  zrhunitpreima  28831  esumpfinvallem  28944  imambfm  29133  carsggect  29199  sibfof  29222  sitgclg  29224  eulerpartlemd  29248  eulerpartlemt  29253  eulerpartlemmf  29257  eulerpartlemgvv  29258  eulerpartlemgu  29259  eulerpartlemgf  29261  dstrvprob  29353  dstfrvel  29355  orvclteinc  29357  erdszelem2  29964  erdszelem7  29969  erdszelem8  29970  cvmliftmolem1  30053  cvmliftlem3  30059  cvmliftlem10  30066  cvmliftlem13  30068  cvmliftlem15  30070  cvmlift2lem9  30083  cvmlift3lem6  30096  cvmlift3lem7  30097  mrsub0  30203  mrsubccat  30205  mrsubcn  30206  msubrn  30216  mclsax  30256  mthmblem  30267  mclsppslem  30270  mclspps  30271  nofun  30585  ivthALT  31040  icoreunrn  31807  icoreelrn  31809  heicant  32020  opnmbllem0  32021  mblfinlem1  32022  dvtanlemOLD  32036  itg2addnclem  32038  itg2addnclem2  32039  ftc1cnnc  32061  ftc1anclem7  32068  ftc1anc  32070  ftc2nc  32071  indexdom  32106  cnres2  32140  heibor1lem  32186  grpokerinj  32228  elrfirn  35582  fnwe2lem2  35954  lmhmfgima  35987  arearect  36145  areaquad  36146  funfvima2d  36657  cncmpmax  37393  fidmfisupp  37517  absfun  37611  evthiccabs  37631  limccog  37738  cncficcgt0  37804  dvsinax  37821  fperdvper  37828  dirkercncflem2  38004  fourierdlem20  38027  fourierdlem42  38050  fourierdlem42OLD  38051  fourierdlem63  38071  fourierdlem76  38084  fourierdlem82  38090  fourierdlem93  38101  fourierdlem97  38105  fourierdlem113  38121  fge0iccico  38250  sge0sn  38259  sge0tsms  38260  sge0cl  38261  sge0f1o  38262  sge0isum  38307  pfxco  39019  uhgrfun  39203  subusgr  39411  pthdivtx  39762  pthdlem2lem  39793  elbigolo1  40641
  Copyright terms: Public domain W3C validator