Theorem ffun 6673

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

Syntax hints:   → wi 4  Fun wfun 6494   Fn wfn 6495  ⟶wf 6496

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 6503  df-f 6504

This theorem is referenced by:  ffund  6674  fco  6694  funssxp  6698  f00  6724  f1cof1  6748  fimadmfoALT  6765  dff3  7054  fliftf  7271  fiun  7897  f1iun  7898  fsuppeq  8127  fsuppeqg  8128  pmfun  8796  pmresg  8820  fodomr  9068  ac6sfi  9196  fodomfir  9240  fissuni  9269  fipreima  9270  ffsuppbi  9313  cnfcomlem  9620  tcrank  9808  fseqenlem2  9947  carduniima  10018  infmap2  10139  hsmexlem4  10351  hsmexlem5  10352  axdc3lem2  10373  axdc3lem4  10375  smobeth  10509  fpwwe2lem12  10565  inar1  10698  grur1  10743  nqerid  10856  fcdmnn0fsuppg  12473  zexALT  12520  hashkf  14267  hashgval  14268  revco  14769  ccatco  14770  pfxco  14773  lswco  14774  climdm  15489  isercolllem2  15601  isercolllem3  15602  isercoll  15603  sum0  15656  sumz  15657  fsumsers  15663  isumclim  15692  ntrivcvgfvn0  15834  ntrivcvgtail  15835  zprodn0  15874  iprodclim  15933  znnen  16149  isacs2  17588  isacs5  18483  dprdss  19972  dprd2dlem1  19984  dmdprdsplit2lem  19988  iscnp3  23200  subbascn  23210  cnpnei  23220  cnclima  23224  iscncl  23225  cncls  23230  cnrest2  23242  cnhaus  23310  kgencn3  23514  xkopt  23611  xkococnlem  23615  hmeores  23727  fbasrn  23840  uzrest  23853  rnelfmlem  23908  rnelfm  23909  fmfnfmlem3  23912  fmfnfmlem4  23913  fmfnfm  23914  cnflf2  23959  metcnp  24497  metustsym  24511  cfilucfil  24515  restmetu  24526  qtopbaslem  24714  tgqioo  24756  re2ndc  24757  bndth  24925  tcphcph  25205  ovolficcss  25438  volf  25498  volsup  25525  uniioombllem3a  25553  uniioombllem4  25555  uniioombllem5  25556  dyadmbllem  25568  dyadmbl  25569  opnmbllem  25570  opnmblALT  25572  mbfimaicc  25600  ismbf3d  25623  mbfimaopnlem  25624  mbfimaopn2  25626  i1fima  25647  i1fima2  25648  i1fd  25650  itg1addlem4  25668  dvidlem  25884  dvcnp  25888  dvadd  25911  dvmul  25912  dvaddf  25913  dvmulf  25914  dvco  25919  dvcof  25920  dvcjbr  25921  dvcj  25922  dvrec  25927  dvcnvlem  25948  dvef  25952  dvferm1  25957  dvferm2  25959  c1liplem1  25969  dvcnvrelem2  25991  mdegcl  26042  deg1n0ima  26062  plyco0  26165  plypf1  26185  tayl0  26337  ulmdvlem3  26379  pserdv  26407  dvlog  26628  efopn  26635  relogbf  26769  nofun  27629  madeval  27840  oldf  27845  oldlim  27895  madefi  27921  oldfi  27922  oldfib  28385  subusgr  29374  pthdivtx  29812  pthdlem2lem  29852  cyclnumvtx  29885  issh2  31296  hlimuni  31325  hhsscms  31365  occllem  31390  occl  31391  chscllem4  31727  imaelshi  32145  xrofsup  32857  tocyc01  33211  exsslsb  33773  dimval  33777  dimvalfi  33778  smatrcl  33973  mdetpmtr1  34000  locfinreflem  34017  fsumcvg4  34127  zrhunitpreima  34153  imambfm  34439  carsggect  34495  sibfof  34517  eulerpartlemt  34548  eulerpartlemmf  34552  eulerpartlemgvv  34553  eulerpartlemgf  34556  rpsqrtcn  34770  cardpred  35267  nummin  35268  erdszelem2  35405  erdszelem7  35410  erdszelem8  35411  cvmliftlem15  35511  mrsub0  35729  mrsubccat  35731  mrsubcn  35732  mthmblem  35793  ivthALT  36548  icoreunrn  37608  icoreelrn  37610  curf  37843  curunc  37847  heicant  37900  opnmbllem0  37901  mblfinlem1  37902  itg2addnclem  37916  itg2addnclem2  37917  ftc1anclem7  37944  ftc1anc  37946  ftc2nc  37947  indexdom  37979  cnres2  38008  aks6d1c6lem2  42535  elrfirn  43046  fnwe2lem2  43402  arearect  43566  areaquad  43567  naddcnff  43713  dfno2  43778  relpfr  45304  absfun  45703  evthiccabs  45850  ioofun  45905  cncficcgt0  46240  fperdvper  46271  fvvolioof  46341  fvvolicof  46343  fourierdlem20  46479  fourierdlem42  46501  fourierdlem63  46521  fourierdlem76  46534  fourierdlem93  46551  fourierdlem97  46555  fourierdlem113  46571  ovolval3  46999  tannpoly  47244  sinnpoly  47245  uniimafveqt  47735  fundcmpsurbijinjpreimafv  47761  fundcmpsurbijinj  47764  fundcmpsurinjALT  47766  fmtnoinf  47890  isubgruhgr  48222  upgrimwlklem1  48251  elbigolo1  48911