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

Theorem ffun 5715
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 5713 . 2  |-  ( F : A --> B  ->  F  Fn  A )
2 fnfun 5660 . 2  |-  ( F  Fn  A  ->  Fun  F )
31, 2syl 16 1  |-  ( F : A --> B  ->  Fun  F )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   Fun wfun 5564    Fn wfn 5565   -->wf 5566
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 185  df-an 369  df-fn 5573  df-f 5574
This theorem is referenced by:  funssxp  5726  f00  5749  fofun  5778  fimacnv  5995  dff3  6020  fmptco  6040  fliftf  6188  fun11iun  6733  frnsuppeq  6903  smores2  7017  pmfun  7431  elmapfun  7435  pmresg  7439  fodomr  7661  ac6sfi  7756  fissuni  7817  fipreima  7818  fdmfifsupp  7831  frnfsuppbi  7850  fsuppmptif  7851  fsuppco2  7854  fsuppcor  7855  ordtypelem8  7942  ordtypelem9  7943  ordtypelem10  7944  unxpwdom2  8006  cantnffvalOLD  8073  cnfcomlem  8134  cnfcomlemOLD  8142  tcrank  8293  fseqenlem2  8397  carduniima  8468  infmap2  8589  hsmexlem4  8800  hsmexlem5  8801  axdc3lem2  8822  axdc3lem4  8824  smobeth  8952  fpwwe2lem13  9009  fpwwe2  9010  inar1  9142  grur1  9187  nqerid  9300  nn0suppOLD  10846  zexALT  10879  hashkf  12392  hashgval  12393  hashfzdm  12485  hashfirdm  12487  revco  12794  ccatco  12795  lswco  12798  climdm  13462  isercolllem2  13573  isercolllem3  13574  isercoll  13575  sum0  13628  sumz  13629  fsumsers  13635  isumclim  13657  ntrivcvgfvn0  13793  ntrivcvgtail  13794  zprodn0  13831  iprodclim  13876  znnen  14033  mrcuni  15113  isacs2  15145  isacs5  16004  cntzmhm2  16579  frgpupval  16994  gsumzadd  17137  gsumpt  17187  gsum2dlem2  17197  dprdss  17274  dprd2dlem1  17288  dprd2da  17289  dmdprdsplit2lem  17292  lmhmpreima  17892  lmhmlsp  17893  psrelbasfun  18231  mplvalOLD  18283  mvrcl  18309  evlslem3  18381  evlseu  18383  mpfind  18403  gsumply1subr  18473  cygznlem2  18783  frlmup1  19003  frlmup4  19006  lindff1  19025  lindfrn  19026  iscnp3  19915  subbascn  19925  cnpnei  19935  cnclima  19939  iscncl  19940  cnclsi  19943  cncls  19945  cncnp  19951  cnrest2  19957  paste  19965  cnhaus  20025  conima  20095  1stcfb  20115  1stccnp  20132  1stckgenlem  20223  kgencn3  20228  txcnpi  20278  txcnp  20290  xkopt  20325  xkoco2cn  20328  xkococnlem  20329  hmeores  20441  fbasrn  20554  uzrest  20567  rnelfmlem  20622  rnelfm  20623  fmfnfmlem2  20625  fmfnfmlem3  20626  fmfnfmlem4  20627  fmfnfm  20628  cnflf2  20673  lmflf  20675  txflf  20676  cnextcn  20736  clssubg  20776  ghmcnp  20782  metcnp  21213  metustidOLD  21231  metustid  21232  metustsymOLD  21233  metustsym  21234  metustexhalfOLD  21235  metustexhalf  21236  cfilucfilOLD  21241  cfilucfil  21242  restmetu  21259  isngp2  21286  qtopbaslem  21434  tgqioo  21474  re2ndc  21475  bndth  21627  pi1xfrval  21723  pi1coval  21729  tchcph  21849  iscfil2  21874  rrxcph  21993  ovolficcss  22050  volf  22109  volsup  22135  uniioombllem3a  22162  uniioombllem4  22164  uniioombllem5  22165  dyadmbllem  22177  dyadmbl  22178  opnmbllem  22179  opnmblALT  22181  mbfimaicc  22209  ismbfd  22216  ismbf3d  22230  mbfimaopnlem  22231  mbfimaopn2  22233  i1fima  22254  i1fima2  22255  i1fd  22257  itg1addlem4  22275  ellimc2  22450  ellimc3  22452  dvres3  22486  dvres3a  22487  dvidlem  22488  dvcnp  22491  dvadd  22512  dvmul  22513  dvaddf  22514  dvmulf  22515  dvco  22519  dvcof  22520  dvcjbr  22521  dvcj  22522  dvrec  22527  dvcnvlem  22546  dvcnv  22547  dvef  22550  dvferm1  22555  dvferm2  22557  c1liplem1  22566  dvcnvrelem1  22587  dvcnvrelem2  22588  ftc1cn  22613  mdegldg  22635  mdegcl  22638  deg1n0ima  22658  plyco0  22758  plyeq0  22777  plypf1  22778  plyaddlem1  22779  plymullem1  22780  tayl0  22926  ulmdvlem3  22966  ulmdv  22967  pserdv  22993  dvlog  23203  efopn  23210  relogbf  23333  dchrelbas2  23713  dchrghm  23732  uhgrafun  24505  eupap1  25181  ghsubgolemOLD  25573  sspg  25842  ssps  25844  sspn  25850  htthlem  26035  issh2  26327  hlimuni  26357  hhsscms  26396  occllem  26422  occl  26423  chscllem4  26759  imaelshi  27178  fmptcof2  27727  curry2ima  27758  fpwrelmapffslem  27789  xrofsup  27819  xrge0tsmsd  28013  locfinreflem  28081  fsumcvg4  28170  zrhunitpreima  28196  esumpfinvallem  28306  imambfm  28473  carsggect  28529  sibfof  28549  sitgclg  28551  eulerpartlemd  28572  eulerpartlemt  28577  eulerpartlemmf  28581  eulerpartlemgvv  28582  eulerpartlemgu  28583  eulerpartlemgf  28585  dstrvprob  28677  dstfrvel  28679  orvclteinc  28681  erdszelem2  28903  erdszelem7  28908  erdszelem8  28909  cvmliftmolem1  28993  cvmliftlem3  28999  cvmliftlem10  29006  cvmliftlem13  29008  cvmliftlem15  29010  cvmlift2lem9  29023  cvmlift3lem6  29036  cvmlift3lem7  29037  mrsub0  29143  mrsubccat  29145  mrsubcn  29146  msubrn  29156  mclsax  29196  mthmblem  29207  mclsppslem  29210  mclspps  29211  nofun  29652  heicant  30292  opnmbllem0  30293  mblfinlem1  30294  dvtanlem  30307  itg2addnclem  30309  itg2addnclem2  30310  ftc1cnnc  30332  ftc1anclem7  30339  ftc1anc  30341  ftc2nc  30342  ivthALT  30396  indexdom  30468  cnres2  30502  heibor1lem  30548  grpokerinj  30590  elrfirn  30870  fnwe2lem2  31239  lmhmfgima  31272  fsuppeq  31285  arearect  31427  areaquad  31428  cncmpmax  31650  evthiccabs  31771  limccog  31868  cncficcgt0  31933  dvsinax  31950  fperdvper  31957  dirkercncflem2  32128  fourierdlem20  32151  fourierdlem42  32173  fourierdlem63  32194  fourierdlem76  32207  fourierdlem82  32213  fourierdlem93  32224  fourierdlem97  32228  fourierdlem113  32244  pfxco  32685  elbigolo1  33451  funfvima2d  38517
  Copyright terms: Public domain W3C validator