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  7038  fliftf  7256  fiun  7885  f1iun  7886  fsuppeq  8115  fsuppeqg  8116  pmfun  8781  pmresg  8804  fodomr  9052  ac6sfi  9189  fodomfir  9237  fissuni  9266  fipreima  9267  ffsuppbi  9307  cnfcomlem  9614  tcrank  9799  fseqenlem2  9938  carduniima  10009  infmap2  10130  hsmexlem4  10342  hsmexlem5  10343  axdc3lem2  10364  axdc3lem4  10366  smobeth  10499  fpwwe2lem12  10555  inar1  10688  grur1  10733  nqerid  10846  fcdmnn0fsuppg  12462  zexALT  12509  hashkf  14257  hashgval  14258  revco  14759  ccatco  14760  pfxco  14763  lswco  14764  climdm  15479  isercolllem2  15591  isercolllem3  15592  isercoll  15593  sum0  15646  sumz  15647  fsumsers  15653  isumclim  15682  ntrivcvgfvn0  15824  ntrivcvgtail  15825  zprodn0  15864  iprodclim  15923  znnen  16139  isacs2  17577  isacs5  18472  dprdss  19928  dprd2dlem1  19940  dmdprdsplit2lem  19944  iscnp3  23147  subbascn  23157  cnpnei  23167  cnclima  23171  iscncl  23172  cncls  23177  cnrest2  23189  cnhaus  23257  kgencn3  23461  xkopt  23558  xkococnlem  23562  hmeores  23674  fbasrn  23787  uzrest  23800  rnelfmlem  23855  rnelfm  23856  fmfnfmlem3  23859  fmfnfmlem4  23860  fmfnfm  23861  cnflf2  23906  metcnp  24445  metustsym  24459  cfilucfil  24463  restmetu  24474  qtopbaslem  24662  tgqioo  24704  re2ndc  24705  bndth  24873  tcphcph  25153  ovolficcss  25386  volf  25446  volsup  25473  uniioombllem3a  25501  uniioombllem4  25503  uniioombllem5  25504  dyadmbllem  25516  dyadmbl  25517  opnmbllem  25518  opnmblALT  25520  mbfimaicc  25548  ismbf3d  25571  mbfimaopnlem  25572  mbfimaopn2  25574  i1fima  25595  i1fima2  25596  i1fd  25598  itg1addlem4  25616  dvidlem  25832  dvcnp  25836  dvadd  25859  dvmul  25860  dvaddf  25861  dvmulf  25862  dvco  25867  dvcof  25868  dvcjbr  25869  dvcj  25870  dvrec  25875  dvcnvlem  25896  dvef  25900  dvferm1  25905  dvferm2  25907  c1liplem1  25917  dvcnvrelem2  25939  mdegcl  25990  deg1n0ima  26010  plyco0  26113  plypf1  26133  tayl0  26285  ulmdvlem3  26327  pserdv  26355  dvlog  26576  efopn  26583  relogbf  26717  nofun  27577  madeval  27780  oldf  27785  oldlim  27819  madefi  27845  oldfi  27846  subusgr  29252  pthdivtx  29690  pthdlem2lem  29730  cyclnumvtx  29763  issh2  31171  hlimuni  31200  hhsscms  31240  occllem  31265  occl  31266  chscllem4  31602  imaelshi  32020  xrofsup  32723  tocyc01  33073  exsslsb  33568  dimval  33572  dimvalfi  33573  smatrcl  33762  mdetpmtr1  33789  locfinreflem  33806  fsumcvg4  33916  zrhunitpreima  33942  imambfm  34229  carsggect  34285  sibfof  34307  eulerpartlemt  34338  eulerpartlemmf  34342  eulerpartlemgvv  34343  eulerpartlemgf  34346  rpsqrtcn  34560  cardpred  35056  nummin  35057  erdszelem2  35164  erdszelem7  35169  erdszelem8  35170  cvmliftlem15  35270  mrsub0  35488  mrsubccat  35490  mrsubcn  35491  mthmblem  35552  ivthALT  36308  icoreunrn  37332  icoreelrn  37334  curf  37577  curunc  37581  heicant  37634  opnmbllem0  37635  mblfinlem1  37636  itg2addnclem  37650  itg2addnclem2  37651  ftc1anclem7  37678  ftc1anc  37680  ftc2nc  37681  indexdom  37713  cnres2  37742  aks6d1c6lem2  42144  elrfirn  42668  fnwe2lem2  43024  arearect  43188  areaquad  43189  naddcnff  43335  dfno2  43401  relpfr  44928  absfun  45330  evthiccabs  45478  ioofun  45533  cncficcgt0  45870  fperdvper  45901  fvvolioof  45971  fvvolicof  45973  fourierdlem20  46109  fourierdlem42  46131  fourierdlem63  46151  fourierdlem76  46164  fourierdlem93  46181  fourierdlem97  46185  fourierdlem113  46201  ovolval3  46629  tannpoly  46875  sinnpoly  46876  uniimafveqt  47366  fundcmpsurbijinjpreimafv  47392  fundcmpsurbijinj  47395  fundcmpsurinjALT  47397  fmtnoinf  47521  isubgruhgr  47853  upgrimwlklem1  47882  elbigolo1  48543