Theorem ffun 6519

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

Syntax hints:   → wi 4  Fun wfun 6351   Fn wfn 6352  ⟶wf 6353

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 209  df-an 399  df-fn 6360  df-f 6361

This theorem is referenced by:  ffund  6520  funssxp  6537  f00  6563  fimadmfoALT  6603  fimacnv  6841  dff3  6868  fliftf  7070  fiun  7646  f1iun  7647  frnsuppeq  7844  pmfun  8428  pmresg  8436  fodomr  8670  ac6sfi  8764  fissuni  8831  fipreima  8832  frnfsuppbi  8864  cnfcomlem  9164  tcrank  9315  fseqenlem2  9453  carduniima  9524  infmap2  9642  hsmexlem4  9853  hsmexlem5  9854  axdc3lem2  9875  axdc3lem4  9877  smobeth  10010  fpwwe2lem13  10066  inar1  10199  grur1  10244  nqerid  10357  zexALT  12004  hashkf  13695  hashgval  13696  revco  14198  ccatco  14199  pfxco  14202  lswco  14203  climdm  14913  isercolllem2  15024  isercolllem3  15025  isercoll  15026  sum0  15080  sumz  15081  fsumsers  15087  isumclim  15114  ntrivcvgfvn0  15257  ntrivcvgtail  15258  zprodn0  15295  iprodclim  15354  znnen  15567  isacs2  16926  isacs5  17784  dprdss  19153  dprd2dlem1  19165  dmdprdsplit2lem  19169  iscnp3  21854  subbascn  21864  cnpnei  21874  cnclima  21878  iscncl  21879  cncls  21884  cnrest2  21896  cnhaus  21964  kgencn3  22168  xkopt  22265  xkococnlem  22269  hmeores  22381  fbasrn  22494  uzrest  22507  rnelfmlem  22562  rnelfm  22563  fmfnfmlem3  22566  fmfnfmlem4  22567  fmfnfm  22568  cnflf2  22613  metcnp  23153  metustsym  23167  cfilucfil  23171  restmetu  23182  qtopbaslem  23369  tgqioo  23410  re2ndc  23411  bndth  23564  tcphcph  23842  ovolficcss  24072  volf  24132  volsup  24159  uniioombllem3a  24187  uniioombllem4  24189  uniioombllem5  24190  dyadmbllem  24202  dyadmbl  24203  opnmbllem  24204  opnmblALT  24206  mbfimaicc  24234  ismbf3d  24257  mbfimaopnlem  24258  mbfimaopn2  24260  i1fima  24281  i1fima2  24282  i1fd  24284  itg1addlem4  24302  dvidlem  24515  dvcnp  24518  dvadd  24539  dvmul  24540  dvaddf  24541  dvmulf  24542  dvco  24546  dvcof  24547  dvcjbr  24548  dvcj  24549  dvrec  24554  dvcnvlem  24575  dvef  24579  dvferm1  24584  dvferm2  24586  c1liplem1  24595  dvcnvrelem2  24617  mdegcl  24665  deg1n0ima  24685  plyco0  24784  plypf1  24804  tayl0  24952  ulmdvlem3  24992  pserdv  25019  dvlog  25236  efopn  25243  relogbf  25371  subusgr  27073  pthdivtx  27512  pthdlem2lem  27550  issh2  28988  hlimuni  29017  hhsscms  29057  occllem  29082  occl  29083  chscllem4  29419  imaelshi  29837  xrofsup  30494  tocyc01  30762  dimval  31003  dimvalfi  31004  smatrcl  31063  mdetpmtr1  31090  locfinreflem  31106  fsumcvg4  31195  zrhunitpreima  31221  imambfm  31522  carsggect  31578  sibfof  31600  eulerpartlemt  31631  eulerpartlemmf  31635  eulerpartlemgvv  31636  eulerpartlemgf  31639  rpsqrtcn  31866  erdszelem2  32441  erdszelem7  32446  erdszelem8  32447  cvmliftlem15  32547  mrsub0  32765  mrsubccat  32767  mrsubcn  32768  mthmblem  32829  nofun  33158  madeval  33291  ivthALT  33685  icoreunrn  34642  icoreelrn  34644  curf  34872  curunc  34876  heicant  34929  opnmbllem0  34930  mblfinlem1  34931  itg2addnclem  34945  itg2addnclem2  34946  ftc1anclem7  34975  ftc1anc  34977  ftc2nc  34978  indexdom  35011  cnres2  35043  elrfirn  39299  fnwe2lem2  39658  arearect  39829  areaquad  39830  absfun  41625  evthiccabs  41778  ioofun  41834  cncficcgt0  42178  fperdvper  42210  fvvolioof  42281  fvvolicof  42283  fourierdlem20  42419  fourierdlem42  42441  fourierdlem63  42461  fourierdlem76  42474  fourierdlem93  42491  fourierdlem97  42495  fourierdlem113  42511  ovolval3  42936  uniimafveqt  43548  fundcmpsurbijinjpreimafv  43574  fundcmpsurbijinj  43577  fundcmpsurinjALT  43579  fmtnoinf  43705  elbigolo1  44624