Theorem ffun 6587

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 6584	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnfun 6517	. 2 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹)

Syntax hints:   → wi 4  Fun wfun 6412   Fn wfn 6413  ⟶wf 6414

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 206  df-an 396  df-fn 6421  df-f 6422

This theorem is referenced by:  ffund  6588  fco  6608  funssxp  6613  f00  6640  f1cof1  6665  fimadmfoALT  6683  fimacnvOLD  6930  dff3  6958  fliftf  7166  fiun  7759  f1iun  7760  frnsuppeq  7962  frnsuppeqg  7963  pmfun  8593  pmresg  8616  fodomr  8864  ac6sfi  8988  fissuni  9054  fipreima  9055  frnfsuppbi  9087  cnfcomlem  9387  tcrank  9573  fseqenlem2  9712  carduniima  9783  infmap2  9905  hsmexlem4  10116  hsmexlem5  10117  axdc3lem2  10138  axdc3lem4  10140  smobeth  10273  fpwwe2lem12  10329  inar1  10462  grur1  10507  nqerid  10620  frnnn0fsuppg  12222  zexALT  12269  hashkf  13974  hashgval  13975  revco  14475  ccatco  14476  pfxco  14479  lswco  14480  climdm  15191  isercolllem2  15305  isercolllem3  15306  isercoll  15307  sum0  15361  sumz  15362  fsumsers  15368  isumclim  15397  ntrivcvgfvn0  15539  ntrivcvgtail  15540  zprodn0  15577  iprodclim  15636  znnen  15849  isacs2  17279  isacs5  18181  dprdss  19547  dprd2dlem1  19559  dmdprdsplit2lem  19563  iscnp3  22303  subbascn  22313  cnpnei  22323  cnclima  22327  iscncl  22328  cncls  22333  cnrest2  22345  cnhaus  22413  kgencn3  22617  xkopt  22714  xkococnlem  22718  hmeores  22830  fbasrn  22943  uzrest  22956  rnelfmlem  23011  rnelfm  23012  fmfnfmlem3  23015  fmfnfmlem4  23016  fmfnfm  23017  cnflf2  23062  metcnp  23603  metustsym  23617  cfilucfil  23621  restmetu  23632  qtopbaslem  23828  tgqioo  23869  re2ndc  23870  bndth  24027  tcphcph  24306  ovolficcss  24538  volf  24598  volsup  24625  uniioombllem3a  24653  uniioombllem4  24655  uniioombllem5  24656  dyadmbllem  24668  dyadmbl  24669  opnmbllem  24670  opnmblALT  24672  mbfimaicc  24700  ismbf3d  24723  mbfimaopnlem  24724  mbfimaopn2  24726  i1fima  24747  i1fima2  24748  i1fd  24750  itg1addlem4  24768  itg1addlem4OLD  24769  dvidlem  24984  dvcnp  24988  dvadd  25009  dvmul  25010  dvaddf  25011  dvmulf  25012  dvco  25016  dvcof  25017  dvcjbr  25018  dvcj  25019  dvrec  25024  dvcnvlem  25045  dvef  25049  dvferm1  25054  dvferm2  25056  c1liplem1  25065  dvcnvrelem2  25087  mdegcl  25139  deg1n0ima  25159  plyco0  25258  plypf1  25278  tayl0  25426  ulmdvlem3  25466  pserdv  25493  dvlog  25711  efopn  25718  relogbf  25846  subusgr  27559  pthdivtx  27998  pthdlem2lem  28036  issh2  29472  hlimuni  29501  hhsscms  29541  occllem  29566  occl  29567  chscllem4  29903  imaelshi  30321  xrofsup  30992  tocyc01  31287  dimval  31588  dimvalfi  31589  smatrcl  31648  mdetpmtr1  31675  locfinreflem  31692  fsumcvg4  31802  zrhunitpreima  31828  imambfm  32129  carsggect  32185  sibfof  32207  eulerpartlemt  32238  eulerpartlemmf  32242  eulerpartlemgvv  32243  eulerpartlemgf  32246  rpsqrtcn  32473  cardpred  32962  nummin  32963  erdszelem2  33054  erdszelem7  33059  erdszelem8  33060  cvmliftlem15  33160  mrsub0  33378  mrsubccat  33380  mrsubcn  33381  mthmblem  33442  nofun  33779  madeval  33963  oldf  33968  oldlim  33996  ivthALT  34451  icoreunrn  35457  icoreelrn  35459  curf  35682  curunc  35686  heicant  35739  opnmbllem0  35740  mblfinlem1  35741  itg2addnclem  35755  itg2addnclem2  35756  ftc1anclem7  35783  ftc1anc  35785  ftc2nc  35786  indexdom  35819  cnres2  35848  elrfirn  40433  fnwe2lem2  40792  arearect  40962  areaquad  40963  absfun  42779  evthiccabs  42924  ioofun  42979  cncficcgt0  43319  fperdvper  43350  fvvolioof  43420  fvvolicof  43422  fourierdlem20  43558  fourierdlem42  43580  fourierdlem63  43600  fourierdlem76  43613  fourierdlem93  43630  fourierdlem97  43634  fourierdlem113  43650  ovolval3  44075  uniimafveqt  44721  fundcmpsurbijinjpreimafv  44747  fundcmpsurbijinj  44750  fundcmpsurinjALT  44752  fmtnoinf  44876  elbigolo1  45791