Theorem ffun 6659

Description: A mapping is a function. (Contributed by NM, 3-Aug-1994.)

Assertion

Ref	Expression
ffun	⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹)

Proof of Theorem ffun

Step	Hyp	Ref	Expression
1		ffn 6656	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnfun 6586	. 2 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹)

Syntax hints:   → wi 4  Fun wfun 6480   Fn wfn 6481  ⟶wf 6482

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 207  df-an 396  df-fn 6489  df-f 6490

This theorem is referenced by:  ffund  6660  fco  6680  funssxp  6684  f00  6710  f1cof1  6734  fimadmfoALT  6751  dff3  7039  fliftf  7255  fiun  7881  f1iun  7882  fsuppeq  8111  fsuppeqg  8112  pmfun  8777  pmresg  8800  fodomr  9048  ac6sfi  9175  fodomfir  9219  fissuni  9248  fipreima  9249  ffsuppbi  9289  cnfcomlem  9596  tcrank  9784  fseqenlem2  9923  carduniima  9994  infmap2  10115  hsmexlem4  10327  hsmexlem5  10328  axdc3lem2  10349  axdc3lem4  10351  smobeth  10484  fpwwe2lem12  10540  inar1  10673  grur1  10718  nqerid  10831  fcdmnn0fsuppg  12448  zexALT  12495  hashkf  14241  hashgval  14242  revco  14743  ccatco  14744  pfxco  14747  lswco  14748  climdm  15463  isercolllem2  15575  isercolllem3  15576  isercoll  15577  sum0  15630  sumz  15631  fsumsers  15637  isumclim  15666  ntrivcvgfvn0  15808  ntrivcvgtail  15809  zprodn0  15848  iprodclim  15907  znnen  16123  isacs2  17561  isacs5  18456  dprdss  19945  dprd2dlem1  19957  dmdprdsplit2lem  19961  iscnp3  23160  subbascn  23170  cnpnei  23180  cnclima  23184  iscncl  23185  cncls  23190  cnrest2  23202  cnhaus  23270  kgencn3  23474  xkopt  23571  xkococnlem  23575  hmeores  23687  fbasrn  23800  uzrest  23813  rnelfmlem  23868  rnelfm  23869  fmfnfmlem3  23872  fmfnfmlem4  23873  fmfnfm  23874  cnflf2  23919  metcnp  24457  metustsym  24471  cfilucfil  24475  restmetu  24486  qtopbaslem  24674  tgqioo  24716  re2ndc  24717  bndth  24885  tcphcph  25165  ovolficcss  25398  volf  25458  volsup  25485  uniioombllem3a  25513  uniioombllem4  25515  uniioombllem5  25516  dyadmbllem  25528  dyadmbl  25529  opnmbllem  25530  opnmblALT  25532  mbfimaicc  25560  ismbf3d  25583  mbfimaopnlem  25584  mbfimaopn2  25586  i1fima  25607  i1fima2  25608  i1fd  25610  itg1addlem4  25628  dvidlem  25844  dvcnp  25848  dvadd  25871  dvmul  25872  dvaddf  25873  dvmulf  25874  dvco  25879  dvcof  25880  dvcjbr  25881  dvcj  25882  dvrec  25887  dvcnvlem  25908  dvef  25912  dvferm1  25917  dvferm2  25919  c1liplem1  25929  dvcnvrelem2  25951  mdegcl  26002  deg1n0ima  26022  plyco0  26125  plypf1  26145  tayl0  26297  ulmdvlem3  26339  pserdv  26367  dvlog  26588  efopn  26595  relogbf  26729  nofun  27589  madeval  27794  oldf  27799  oldlim  27833  madefi  27859  oldfi  27860  subusgr  29269  pthdivtx  29707  pthdlem2lem  29747  cyclnumvtx  29780  issh2  31191  hlimuni  31220  hhsscms  31260  occllem  31285  occl  31286  chscllem4  31622  imaelshi  32040  xrofsup  32754  tocyc01  33094  exsslsb  33630  dimval  33634  dimvalfi  33635  smatrcl  33830  mdetpmtr1  33857  locfinreflem  33874  fsumcvg4  33984  zrhunitpreima  34010  imambfm  34296  carsggect  34352  sibfof  34374  eulerpartlemt  34405  eulerpartlemmf  34409  eulerpartlemgvv  34410  eulerpartlemgf  34413  rpsqrtcn  34627  cardpred  35124  nummin  35125  erdszelem2  35257  erdszelem7  35262  erdszelem8  35263  cvmliftlem15  35363  mrsub0  35581  mrsubccat  35583  mrsubcn  35584  mthmblem  35645  ivthALT  36400  icoreunrn  37424  icoreelrn  37426  curf  37658  curunc  37662  heicant  37715  opnmbllem0  37716  mblfinlem1  37717  itg2addnclem  37731  itg2addnclem2  37732  ftc1anclem7  37759  ftc1anc  37761  ftc2nc  37762  indexdom  37794  cnres2  37823  aks6d1c6lem2  42284  elrfirn  42812  fnwe2lem2  43168  arearect  43332  areaquad  43333  naddcnff  43479  dfno2  43545  relpfr  45071  absfun  45473  evthiccabs  45620  ioofun  45675  cncficcgt0  46010  fperdvper  46041  fvvolioof  46111  fvvolicof  46113  fourierdlem20  46249  fourierdlem42  46271  fourierdlem63  46291  fourierdlem76  46304  fourierdlem93  46321  fourierdlem97  46325  fourierdlem113  46341  ovolval3  46769  tannpoly  47014  sinnpoly  47015  uniimafveqt  47505  fundcmpsurbijinjpreimafv  47531  fundcmpsurbijinj  47534  fundcmpsurinjALT  47536  fmtnoinf  47660  isubgruhgr  47992  upgrimwlklem1  48021  elbigolo1  48682