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

Theorem ffun 5947
Description: A mapping is a function. (Contributed by NM, 3-Aug-1994.)
Assertion
Ref Expression
ffun (𝐹:𝐴𝐵 → Fun 𝐹)

Proof of Theorem ffun
StepHypRef Expression
1 ffn 5944 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 fnfun 5888 . 2 (𝐹 Fn 𝐴 → Fun 𝐹)
31, 2syl 17 1 (𝐹:𝐴𝐵 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Fun wfun 5784   Fn wfn 5785  wf 5786
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 195  df-an 384  df-fn 5793  df-f 5794
This theorem is referenced by:  ffund  5948  funssxp  5960  f00  5985  fofun  6014  fimacnv  6240  dff3  6265  fliftf  6443  fun11iun  6996  frnsuppeq  7171  smores2  7315  pmfun  7740  elmapfun  7744  pmresg  7748  fodomr  7973  ac6sfi  8066  fissuni  8131  fipreima  8132  fdmfifsupp  8145  frnfsuppbi  8164  fsuppmptif  8165  fsuppco2  8168  fsuppcor  8169  ordtypelem8  8290  ordtypelem9  8291  ordtypelem10  8292  unxpwdom2  8353  cnfcomlem  8456  tcrank  8607  fseqenlem2  8708  carduniima  8779  infmap2  8900  hsmexlem4  9111  hsmexlem5  9112  axdc3lem2  9133  axdc3lem4  9135  smobeth  9264  fpwwe2lem13  9320  fpwwe2  9321  inar1  9453  grur1  9498  nqerid  9611  zexALT  11229  hashkf  12936  hashgval  12937  revco  13377  ccatco  13378  lswco  13381  climdm  14079  isercolllem2  14190  isercolllem3  14191  isercoll  14192  sum0  14245  sumz  14246  fsumsers  14252  isumclim  14276  ntrivcvgfvn0  14416  ntrivcvgtail  14417  zprodn0  14454  iprodclim  14514  znnen  14726  mrcuni  16050  isacs2  16083  isacs5  16941  cntzmhm2  17541  frgpupval  17956  gsumzadd  18091  gsumpt  18130  gsum2dlem2  18139  dprdss  18197  dprd2dlem1  18209  dprd2da  18210  dmdprdsplit2lem  18213  lmhmpreima  18815  lmhmlsp  18816  psrelbasfun  19147  mvrcl  19216  evlseu  19283  mpfind  19303  gsumply1subr  19371  cygznlem2  19681  frlmup1  19898  frlmup4  19901  lindff1  19920  lindfrn  19921  iscnp3  20800  subbascn  20810  cnpnei  20820  cnclima  20824  iscncl  20825  cnclsi  20828  cncls  20830  cncnp  20836  cnrest2  20842  paste  20850  cnhaus  20910  conima  20980  1stcfb  21000  1stccnp  21017  1stckgenlem  21108  kgencn3  21113  txcnpi  21163  txcnp  21175  xkopt  21210  xkoco2cn  21213  xkococnlem  21214  hmeores  21326  fbasrn  21440  uzrest  21453  rnelfmlem  21508  rnelfm  21509  fmfnfmlem2  21511  fmfnfmlem3  21512  fmfnfmlem4  21513  fmfnfm  21514  cnflf2  21559  lmflf  21561  txflf  21562  cnextcn  21623  clssubg  21664  ghmcnp  21670  metcnp  22097  metustid  22110  metustsym  22111  metustexhalf  22112  cfilucfil  22115  restmetu  22126  isngp2  22152  qtopbaslem  22304  tgqioo  22343  re2ndc  22344  bndth  22496  pi1xfrval  22593  pi1coval  22599  tchcph  22765  iscfil2  22790  rrxcph  22905  ovolficcss  22962  volf  23021  volsup  23048  uniioombllem3a  23075  uniioombllem4  23077  uniioombllem5  23078  dyadmbllem  23090  dyadmbl  23091  opnmbllem  23092  opnmblALT  23094  mbfimaicc  23123  ismbfd  23130  ismbf3d  23144  mbfimaopnlem  23145  mbfimaopn2  23147  i1fima  23168  i1fima2  23169  i1fd  23171  itg1addlem4  23189  ellimc2  23364  ellimc3  23366  dvres3  23400  dvres3a  23401  dvidlem  23402  dvcnp  23405  dvadd  23426  dvmul  23427  dvaddf  23428  dvmulf  23429  dvco  23433  dvcof  23434  dvcjbr  23435  dvcj  23436  dvrec  23441  dvcnvlem  23460  dvcnv  23461  dvef  23464  dvferm1  23469  dvferm2  23471  c1liplem1  23480  dvcnvrelem1  23501  dvcnvrelem2  23502  ftc1cn  23527  mdegcl  23550  deg1n0ima  23570  plyco0  23669  plyeq0  23688  plypf1  23689  plyaddlem1  23690  plymullem1  23691  tayl0  23837  ulmdvlem3  23877  ulmdv  23878  pserdv  23904  dvlog  24114  efopn  24121  relogbf  24246  dchrelbas2  24679  dchrghm  24698  uhgrafun  25595  eupap1  26269  sspg  26771  ssps  26773  sspn  26779  htthlem  26964  issh2  27256  hlimuni  27285  hhsscms  27326  occllem  27352  occl  27353  chscllem4  27689  imaelshi  28107  fmptcof2  28645  curry2ima  28675  fpwrelmapffslem  28701  xrofsup  28729  xrge0tsmsd  28922  smatrcl  28996  mdetpmtr1  29023  locfinreflem  29041  fsumcvg4  29130  zrhunitpreima  29156  esumpfinvallem  29269  imambfm  29457  carsggect  29513  sibfof  29535  sitgclg  29537  eulerpartlemd  29561  eulerpartlemt  29566  eulerpartlemmf  29570  eulerpartlemgvv  29571  eulerpartlemgu  29572  eulerpartlemgf  29574  dstrvprob  29666  dstfrvel  29668  orvclteinc  29670  erdszelem2  30234  erdszelem7  30239  erdszelem8  30240  cvmliftmolem1  30323  cvmliftlem3  30329  cvmliftlem10  30336  cvmliftlem13  30338  cvmliftlem15  30340  cvmlift2lem9  30353  cvmlift3lem6  30366  cvmlift3lem7  30367  mrsub0  30473  mrsubccat  30475  mrsubcn  30476  msubrn  30486  mclsax  30526  mthmblem  30537  mclsppslem  30540  mclspps  30541  nofun  30852  ivthALT  31306  icoreunrn  32179  icoreelrn  32181  curf  32353  curunc  32357  heicant  32410  opnmbllem0  32411  mblfinlem1  32412  itg2addnclem  32427  itg2addnclem2  32428  ftc1cnnc  32450  ftc1anclem7  32457  ftc1anc  32459  ftc2nc  32460  indexdom  32495  cnres2  32528  heibor1lem  32574  grpokerinj  32658  elrfirn  36072  fnwe2lem2  36435  lmhmfgima  36468  arearect  36616  areaquad  36617  funfvima2d  37287  cncmpmax  38010  fidmfisupp  38181  absfun  38304  evthiccabs  38362  ioofun  38422  limccog  38484  cncficcgt0  38571  dvsinax  38598  fperdvper  38605  fvvolioof  38679  fvvolicof  38681  dirkercncflem2  38794  fourierdlem20  38817  fourierdlem42  38839  fourierdlem63  38859  fourierdlem76  38872  fourierdlem82  38878  fourierdlem93  38889  fourierdlem97  38893  fourierdlem113  38909  fge0iccico  39060  sge0sn  39069  sge0tsms  39070  sge0cl  39071  sge0f1o  39072  sge0isum  39117  ovolval3  39334  ovnovollem1  39343  fmtnoinf  39784  pfxco  40099  uhgrfun  40283  subusgr  40508  vdegp1ai-av  40747  1wlkreslem  40873  pthdivtx  40930  pthdlem2lem  40968  elbigolo1  42144
  Copyright terms: Public domain W3C validator