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

Theorem ffun 5684
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 5682 . 2  |-  ( F : A --> B  ->  F  Fn  A )
2 fnfun 5627 . 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 5531    Fn wfn 5532   -->wf 5533
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 188  df-an 372  df-fn 5540  df-f 5541
This theorem is referenced by:  funssxp  5695  f00  5718  fofun  5747  fimacnv  5964  dff3  5987  fmptco  6008  fliftf  6160  fun11iun  6704  frnsuppeq  6874  smores2  7021  pmfun  7439  elmapfun  7443  pmresg  7447  fodomr  7669  ac6sfi  7761  fissuni  7825  fipreima  7826  fdmfifsupp  7839  frnfsuppbi  7858  fsuppmptif  7859  fsuppco2  7862  fsuppcor  7863  ordtypelem8  7986  ordtypelem9  7987  ordtypelem10  7988  unxpwdom2  8049  cnfcomlem  8149  tcrank  8300  fseqenlem2  8400  carduniima  8471  infmap2  8592  hsmexlem4  8803  hsmexlem5  8804  axdc3lem2  8825  axdc3lem4  8827  smobeth  8955  fpwwe2lem13  9011  fpwwe2  9012  inar1  9144  grur1  9189  nqerid  9302  zexALT  10900  hashkf  12460  hashgval  12461  hashfzdm  12553  hashfirdm  12555  revco  12870  ccatco  12871  lswco  12874  climdm  13554  isercolllem2  13665  isercolllem3  13666  isercoll  13667  sum0  13723  sumz  13724  fsumsers  13730  isumclim  13754  ntrivcvgfvn0  13891  ntrivcvgtail  13892  zprodn0  13929  iprodclim  13987  znnen  14201  mrcuni  15463  isacs2  15495  isacs5  16354  cntzmhm2  16929  frgpupval  17360  gsumzadd  17491  gsumpt  17530  gsum2dlem2  17539  dprdss  17598  dprd2dlem1  17610  dprd2da  17611  dmdprdsplit2lem  17614  lmhmpreima  18207  lmhmlsp  18208  psrelbasfun  18540  mvrcl  18609  evlslem3  18673  evlseu  18675  mpfind  18695  gsumply1subr  18763  cygznlem2  19074  frlmup1  19291  frlmup4  19294  lindff1  19313  lindfrn  19314  iscnp3  20195  subbascn  20205  cnpnei  20215  cnclima  20219  iscncl  20220  cnclsi  20223  cncls  20225  cncnp  20231  cnrest2  20237  paste  20245  cnhaus  20305  conima  20375  1stcfb  20395  1stccnp  20412  1stckgenlem  20503  kgencn3  20508  txcnpi  20558  txcnp  20570  xkopt  20605  xkoco2cn  20608  xkococnlem  20609  hmeores  20721  fbasrn  20834  uzrest  20847  rnelfmlem  20902  rnelfm  20903  fmfnfmlem2  20905  fmfnfmlem3  20906  fmfnfmlem4  20907  fmfnfm  20908  cnflf2  20953  lmflf  20955  txflf  20956  cnextcn  21017  clssubg  21058  ghmcnp  21064  metcnp  21491  metustid  21504  metustsym  21505  metustexhalf  21506  cfilucfil  21509  restmetu  21520  isngp2  21546  qtopbaslem  21714  tgqioo  21753  re2ndc  21754  bndth  21921  pi1xfrval  22020  pi1coval  22026  tchcph  22146  iscfil2  22171  rrxcph  22286  ovolficcss  22357  volf  22418  volsup  22444  uniioombllem3a  22477  uniioombllem4  22479  uniioombllem5  22480  dyadmbllem  22492  dyadmbl  22493  opnmbllem  22494  opnmblALT  22496  mbfimaicc  22524  ismbfd  22531  ismbf3d  22545  mbfimaopnlem  22546  mbfimaopn2  22548  i1fima  22571  i1fima2  22572  i1fd  22574  itg1addlem4  22592  ellimc2  22767  ellimc3  22769  dvres3  22803  dvres3a  22804  dvidlem  22805  dvcnp  22808  dvadd  22829  dvmul  22830  dvaddf  22831  dvmulf  22832  dvco  22836  dvcof  22837  dvcjbr  22838  dvcj  22839  dvrec  22844  dvcnvlem  22863  dvcnv  22864  dvef  22867  dvferm1  22872  dvferm2  22874  c1liplem1  22883  dvcnvrelem1  22904  dvcnvrelem2  22905  ftc1cn  22930  mdegldg  22950  mdegcl  22953  deg1n0ima  22973  plyco0  23081  plyeq0  23100  plypf1  23101  plyaddlem1  23102  plymullem1  23103  tayl0  23252  ulmdvlem3  23292  ulmdv  23293  pserdv  23319  dvlog  23531  efopn  23538  relogbf  23663  dchrelbas2  24100  dchrghm  24119  uhgrafun  24962  eupap1  25639  ghsubgolemOLD  26033  sspg  26302  ssps  26304  sspn  26310  htthlem  26505  issh2  26797  hlimuni  26826  hhsscms  26865  occllem  26891  occl  26892  chscllem4  27228  imaelshi  27646  fmptcof2  28198  curry2ima  28228  fpwrelmapffslem  28260  xrofsup  28296  xrge0tsmsd  28493  smatrcl  28567  mdetpmtr1  28594  locfinreflem  28612  fsumcvg4  28701  zrhunitpreima  28727  esumpfinvallem  28840  imambfm  29029  carsggect  29095  sibfof  29118  sitgclg  29120  eulerpartlemd  29144  eulerpartlemt  29149  eulerpartlemmf  29153  eulerpartlemgvv  29154  eulerpartlemgu  29155  eulerpartlemgf  29157  dstrvprob  29249  dstfrvel  29251  orvclteinc  29253  erdszelem2  29860  erdszelem7  29865  erdszelem8  29866  cvmliftmolem1  29949  cvmliftlem3  29955  cvmliftlem10  29962  cvmliftlem13  29964  cvmliftlem15  29966  cvmlift2lem9  29979  cvmlift3lem6  29992  cvmlift3lem7  29993  mrsub0  30099  mrsubccat  30101  mrsubcn  30102  msubrn  30112  mclsax  30152  mthmblem  30163  mclsppslem  30166  mclspps  30167  nofun  30480  ivthALT  30933  icoreunrn  31663  icoreelrn  31665  heicant  31876  opnmbllem0  31877  mblfinlem1  31878  dvtanlemOLD  31892  itg2addnclem  31894  itg2addnclem2  31895  ftc1cnnc  31917  ftc1anclem7  31924  ftc1anc  31926  ftc2nc  31927  indexdom  31962  cnres2  31996  heibor1lem  32042  grpokerinj  32084  elrfirn  35443  fnwe2lem2  35816  lmhmfgima  35849  arearect  36007  areaquad  36008  funfvima2d  36519  cncmpmax  37263  absfun  37464  evthiccabs  37479  limccog  37577  cncficcgt0  37643  dvsinax  37660  fperdvper  37667  dirkercncflem2  37843  fourierdlem20  37866  fourierdlem42  37889  fourierdlem42OLD  37890  fourierdlem63  37910  fourierdlem76  37923  fourierdlem82  37929  fourierdlem93  37940  fourierdlem97  37944  fourierdlem113  37960  fge0iccico  38057  sge0sn  38066  sge0tsms  38067  sge0cl  38068  sge0f1o  38069  sge0isum  38114  pfxco  38786  uhgrfun  38923  subusgr  39092  elbigolo1  39955
  Copyright terms: Public domain W3C validator