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

Theorem ffun 5748
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 5746 . 2  |-  ( F : A --> B  ->  F  Fn  A )
2 fnfun 5691 . 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 188  df-an 372  df-fn 5604  df-f 5605
This theorem is referenced by:  funssxp  5759  f00  5782  fofun  5811  fimacnv  6027  dff3  6050  fmptco  6071  fliftf  6223  fun11iun  6767  frnsuppeq  6937  smores2  7081  pmfun  7499  elmapfun  7503  pmresg  7507  fodomr  7729  ac6sfi  7821  fissuni  7885  fipreima  7886  fdmfifsupp  7899  frnfsuppbi  7918  fsuppmptif  7919  fsuppco2  7922  fsuppcor  7923  ordtypelem8  8040  ordtypelem9  8041  ordtypelem10  8042  unxpwdom2  8103  cnfcomlem  8203  tcrank  8354  fseqenlem2  8454  carduniima  8525  infmap2  8646  hsmexlem4  8857  hsmexlem5  8858  axdc3lem2  8879  axdc3lem4  8881  smobeth  9009  fpwwe2lem13  9066  fpwwe2  9067  inar1  9199  grur1  9244  nqerid  9357  zexALT  10956  hashkf  12514  hashgval  12515  hashfzdm  12607  hashfirdm  12609  revco  12916  ccatco  12917  lswco  12920  climdm  13596  isercolllem2  13707  isercolllem3  13708  isercoll  13709  sum0  13765  sumz  13766  fsumsers  13772  isumclim  13796  ntrivcvgfvn0  13933  ntrivcvgtail  13934  zprodn0  13971  iprodclim  14029  znnen  14243  mrcuni  15478  isacs2  15510  isacs5  16369  cntzmhm2  16944  frgpupval  17359  gsumzadd  17490  gsumpt  17529  gsum2dlem2  17538  dprdss  17597  dprd2dlem1  17609  dprd2da  17610  dmdprdsplit2lem  17613  lmhmpreima  18206  lmhmlsp  18207  psrelbasfun  18539  mvrcl  18608  evlslem3  18672  evlseu  18674  mpfind  18694  gsumply1subr  18762  cygznlem2  19070  frlmup1  19287  frlmup4  19290  lindff1  19309  lindfrn  19310  iscnp3  20191  subbascn  20201  cnpnei  20211  cnclima  20215  iscncl  20216  cnclsi  20219  cncls  20221  cncnp  20227  cnrest2  20233  paste  20241  cnhaus  20301  conima  20371  1stcfb  20391  1stccnp  20408  1stckgenlem  20499  kgencn3  20504  txcnpi  20554  txcnp  20566  xkopt  20601  xkoco2cn  20604  xkococnlem  20605  hmeores  20717  fbasrn  20830  uzrest  20843  rnelfmlem  20898  rnelfm  20899  fmfnfmlem2  20901  fmfnfmlem3  20902  fmfnfmlem4  20903  fmfnfm  20904  cnflf2  20949  lmflf  20951  txflf  20952  cnextcn  21013  clssubg  21054  ghmcnp  21060  metcnp  21487  metustid  21500  metustsym  21501  metustexhalf  21502  cfilucfil  21505  restmetu  21516  isngp2  21542  qtopbaslem  21690  tgqioo  21729  re2ndc  21730  bndth  21882  pi1xfrval  21978  pi1coval  21984  tchcph  22104  iscfil2  22129  rrxcph  22244  ovolficcss  22301  volf  22360  volsup  22386  uniioombllem3a  22419  uniioombllem4  22421  uniioombllem5  22422  dyadmbllem  22434  dyadmbl  22435  opnmbllem  22436  opnmblALT  22438  mbfimaicc  22466  ismbfd  22473  ismbf3d  22487  mbfimaopnlem  22488  mbfimaopn2  22490  i1fima  22513  i1fima2  22514  i1fd  22516  itg1addlem4  22534  ellimc2  22709  ellimc3  22711  dvres3  22745  dvres3a  22746  dvidlem  22747  dvcnp  22750  dvadd  22771  dvmul  22772  dvaddf  22773  dvmulf  22774  dvco  22778  dvcof  22779  dvcjbr  22780  dvcj  22781  dvrec  22786  dvcnvlem  22805  dvcnv  22806  dvef  22809  dvferm1  22814  dvferm2  22816  c1liplem1  22825  dvcnvrelem1  22846  dvcnvrelem2  22847  ftc1cn  22872  mdegldg  22892  mdegcl  22895  deg1n0ima  22915  plyco0  23014  plyeq0  23033  plypf1  23034  plyaddlem1  23035  plymullem1  23036  tayl0  23182  ulmdvlem3  23222  ulmdv  23223  pserdv  23249  dvlog  23461  efopn  23468  relogbf  23593  dchrelbas2  24028  dchrghm  24047  uhgrafun  24873  eupap1  25549  ghsubgolemOLD  25943  sspg  26212  ssps  26214  sspn  26220  htthlem  26405  issh2  26697  hlimuni  26726  hhsscms  26765  occllem  26791  occl  26792  chscllem4  27128  imaelshi  27546  fmptcof2  28099  curry2ima  28129  fpwrelmapffslem  28160  xrofsup  28189  xrge0tsmsd  28387  smatrcl  28461  mdetpmtr1  28488  locfinreflem  28506  fsumcvg4  28595  zrhunitpreima  28621  esumpfinvallem  28734  imambfm  28923  carsggect  28979  sibfof  29001  sitgclg  29003  eulerpartlemd  29025  eulerpartlemt  29030  eulerpartlemmf  29034  eulerpartlemgvv  29035  eulerpartlemgu  29036  eulerpartlemgf  29038  dstrvprob  29130  dstfrvel  29132  orvclteinc  29134  erdszelem2  29703  erdszelem7  29708  erdszelem8  29709  cvmliftmolem1  29792  cvmliftlem3  29798  cvmliftlem10  29805  cvmliftlem13  29807  cvmliftlem15  29809  cvmlift2lem9  29822  cvmlift3lem6  29835  cvmlift3lem7  29836  mrsub0  29942  mrsubccat  29944  mrsubcn  29945  msubrn  29955  mclsax  29995  mthmblem  30006  mclsppslem  30009  mclspps  30010  nofun  30323  ivthALT  30776  icoreunrn  31496  icoreelrn  31498  heicant  31679  opnmbllem0  31680  mblfinlem1  31681  dvtanlemOLD  31695  itg2addnclem  31697  itg2addnclem2  31698  ftc1cnnc  31720  ftc1anclem7  31727  ftc1anc  31729  ftc2nc  31730  indexdom  31765  cnres2  31799  heibor1lem  31845  grpokerinj  31887  elrfirn  35246  fnwe2lem2  35615  lmhmfgima  35648  arearect  35799  areaquad  35800  funfvima2d  36249  cncmpmax  36993  evthiccabs  37178  limccog  37272  cncficcgt0  37338  dvsinax  37355  fperdvper  37362  dirkercncflem2  37535  fourierdlem20  37558  fourierdlem42  37580  fourierdlem63  37601  fourierdlem76  37614  fourierdlem82  37620  fourierdlem93  37631  fourierdlem97  37635  fourierdlem113  37651  fge0iccico  37746  sge0sn  37755  sge0tsms  37756  sge0cl  37757  sge0f1o  37758  pfxco  38369  elbigolo1  39129
  Copyright terms: Public domain W3C validator