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

Theorem ffun 5549
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 5547 . 2  |-  ( F : A --> B  ->  F  Fn  A )
2 fnfun 5496 . 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 5400    Fn wfn 5401   -->wf 5402
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 371  df-fn 5409  df-f 5410
This theorem is referenced by:  funssxp  5559  f00  5581  fofun  5609  fimacnv  5823  dff3  5844  fmptco  5863  fliftf  5995  fun11iun  6526  frnsuppeq  6691  smores2  6801  pmfun  7220  elmapfun  7224  pmresg  7228  fodomr  7450  ac6sfi  7544  fissuni  7604  fipreima  7605  fdmfifsupp  7618  frnfsuppbi  7636  fsuppmptif  7637  fsuppco2  7640  fsuppcor  7641  ordtypelem8  7727  ordtypelem9  7728  ordtypelem10  7729  unxpwdom2  7791  cantnffvalOLD  7859  cnfcomlem  7920  cnfcomlemOLD  7928  tcrank  8079  fseqenlem2  8183  carduniima  8254  infmap2  8375  hsmexlem4  8586  hsmexlem5  8587  axdc3lem2  8608  axdc3lem4  8610  smobeth  8738  fpwwe2lem13  8796  fpwwe2  8797  inar1  8929  grur1  8974  nqerid  9089  nn0suppOLD  10621  zexALT  10652  hashkf  12088  hashgval  12089  hashfzdm  12185  hashfirdm  12187  revco  12445  ccatco  12446  lswco  12449  climdm  13015  isercolllem2  13126  isercolllem3  13127  isercoll  13128  sum0  13181  sumz  13182  fsumsers  13188  isumclim  13207  znnen  13477  mrcuni  14541  isacs2  14573  isacs5  15324  cntzmhm2  15836  frgpupval  16250  gsumzadd  16388  gsumpt  16428  gsum2dlem2  16435  dprdss  16499  dprd2dlem1  16513  dprd2da  16514  dmdprdsplit2lem  16517  lmhmpreima  17050  lmhmlsp  17051  psrelbasfun  17384  mplvalOLD  17435  mvrcl  17461  ltbwe  17485  cygznlem2  17842  frlmup1  18067  frlmup4  18070  lindff1  18090  lindfrn  18091  iscnp3  18689  subbascn  18699  cnpnei  18709  cnclima  18713  iscncl  18714  cnclsi  18717  cncls  18719  cncnp  18725  cnrest  18730  cnrest2  18731  paste  18739  cnhaus  18799  bwthOLD  18855  conima  18870  1stcfb  18890  1stccnp  18907  1stckgenlem  18967  kgencn3  18972  txcnpi  19022  txcnp  19034  xkopt  19069  xkoco2cn  19072  xkococnlem  19073  hmeores  19185  fbasrn  19298  uzrest  19311  rnelfmlem  19366  rnelfm  19367  fmfnfmlem2  19369  fmfnfmlem3  19370  fmfnfmlem4  19371  fmfnfm  19372  cnflf2  19417  lmflf  19419  txflf  19420  cnextcn  19480  clssubg  19520  ghmcnp  19526  metcnp  19957  metustidOLD  19975  metustid  19976  metustsymOLD  19977  metustsym  19978  metustexhalfOLD  19979  metustexhalf  19980  cfilucfilOLD  19985  cfilucfil  19986  restmetu  20003  isngp2  20030  qtopbaslem  20178  tgqioo  20218  re2ndc  20219  bndth  20371  pi1xfrval  20467  pi1coval  20473  tchcph  20593  iscfil2  20618  rrxcph  20737  ovolficcss  20794  volf  20853  volsup  20878  uniioombllem3a  20905  uniioombllem4  20907  uniioombllem5  20908  dyadmbllem  20920  dyadmbl  20921  opnmbllem  20922  opnmblALT  20924  mbfimaicc  20952  ismbfd  20959  ismbf3d  20973  mbfimaopnlem  20974  mbfimaopn2  20976  i1fima  20997  i1fima2  20998  i1fd  21000  itg1addlem4  21018  ellimc2  21193  ellimc3  21195  dvres3  21229  dvres3a  21230  dvidlem  21231  dvcnp  21234  dvadd  21255  dvmul  21256  dvaddf  21257  dvmulf  21258  dvco  21262  dvcof  21263  dvcjbr  21264  dvcj  21265  dvrec  21270  dvcnvlem  21289  dvcnv  21290  dvef  21293  dvferm1  21298  dvferm2  21300  c1liplem1  21309  dvcnvrelem1  21330  dvcnvrelem2  21331  ftc1cn  21356  evlslem3  21365  evlseu  21367  mpfind  21395  mdegldg  21421  mdegcl  21424  deg1n0ima  21444  plyco0  21544  plyeq0  21563  plypf1  21564  plyaddlem1  21565  plymullem1  21566  tayl0  21711  ulmdvlem3  21751  ulmdv  21752  pserdv  21778  dvlog  21980  efopn  21987  dchrelbas2  22460  dchrghm  22479  uhgrafun  23061  eupap1  23419  ghsubgolem  23679  sspg  23948  ssps  23950  sspn  23956  htthlem  24141  issh2  24433  hlimuni  24463  hhsscms  24502  occllem  24528  occl  24529  chscllem4  24865  imaelshi  25284  fmptcof2  25802  curry2ima  25826  nn0supp  25851  ffs2  25852  fpwrelmapffslem  25856  xrofsup  25877  fsumcvg4  26233  zrhunitpreima  26260  esumpfinvallem  26376  mbfmfun  26522  imambfm  26530  sibfof  26573  sitgclg  26575  eulerpartlemd  26596  eulerpartlemt  26601  eulerpartgbij  26602  eulerpartlemmf  26605  eulerpartlemgvv  26606  eulerpartlemgu  26607  eulerpartlemgf  26609  dstrvprob  26701  dstfrvel  26703  orvclteinc  26705  erdszelem2  26927  erdszelem7  26932  erdszelem8  26933  cvmliftmolem1  27017  cvmliftlem3  27023  cvmliftlem10  27030  cvmliftlem13  27032  cvmliftlem15  27034  cvmlift2lem9  27047  cvmlift3lem6  27060  cvmlift3lem7  27061  ntrivcvgfvn0  27260  ntrivcvgtail  27261  zprodn0  27298  iprodclim  27344  nofun  27636  heicant  28267  opnmbllem0  28268  mblfinlem1  28269  dvtanlem  28282  itg2addnclem  28284  itg2addnclem2  28285  ftc1cnnc  28307  ftc1anclem7  28314  ftc1anc  28316  ftc2nc  28317  ivthALT  28371  indexdom  28469  cnres2  28503  heibor1lem  28549  grpokerinj  28591  elrfirn  28873  fnwe2lem2  29246  lmhmfgima  29279  fsuppeq  29292  arearect  29433  areaquad  29434  cncmpmax  29596  domnmsuppn0  30610  rmsuppss  30611  mndpsuppss  30612  scmsuppss  30613
  Copyright terms: Public domain W3C validator