Theorem ffun 6612

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

Syntax hints:   → wi 4  Fun wfun 6431   Fn wfn 6432  ⟶wf 6433

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 397  df-fn 6440  df-f 6441

This theorem is referenced by:  ffund  6613  fco  6633  funssxp  6638  f00  6665  f1cof1  6690  fimadmfoALT  6708  fimacnvOLD  6957  dff3  6985  fliftf  7195  fiun  7794  f1iun  7795  frnsuppeq  8000  frnsuppeqg  8001  pmfun  8644  pmresg  8667  fodomr  8924  ac6sfi  9067  fissuni  9133  fipreima  9134  frnfsuppbi  9166  cnfcomlem  9466  tcrank  9651  fseqenlem2  9790  carduniima  9861  infmap2  9983  hsmexlem4  10194  hsmexlem5  10195  axdc3lem2  10216  axdc3lem4  10218  smobeth  10351  fpwwe2lem12  10407  inar1  10540  grur1  10585  nqerid  10698  frnnn0fsuppg  12301  zexALT  12348  hashkf  14055  hashgval  14056  revco  14556  ccatco  14557  pfxco  14560  lswco  14561  climdm  15272  isercolllem2  15386  isercolllem3  15387  isercoll  15388  sum0  15442  sumz  15443  fsumsers  15449  isumclim  15478  ntrivcvgfvn0  15620  ntrivcvgtail  15621  zprodn0  15658  iprodclim  15717  znnen  15930  isacs2  17371  isacs5  18275  dprdss  19641  dprd2dlem1  19653  dmdprdsplit2lem  19657  iscnp3  22404  subbascn  22414  cnpnei  22424  cnclima  22428  iscncl  22429  cncls  22434  cnrest2  22446  cnhaus  22514  kgencn3  22718  xkopt  22815  xkococnlem  22819  hmeores  22931  fbasrn  23044  uzrest  23057  rnelfmlem  23112  rnelfm  23113  fmfnfmlem3  23116  fmfnfmlem4  23117  fmfnfm  23118  cnflf2  23163  metcnp  23706  metustsym  23720  cfilucfil  23724  restmetu  23735  qtopbaslem  23931  tgqioo  23972  re2ndc  23973  bndth  24130  tcphcph  24410  ovolficcss  24642  volf  24702  volsup  24729  uniioombllem3a  24757  uniioombllem4  24759  uniioombllem5  24760  dyadmbllem  24772  dyadmbl  24773  opnmbllem  24774  opnmblALT  24776  mbfimaicc  24804  ismbf3d  24827  mbfimaopnlem  24828  mbfimaopn2  24830  i1fima  24851  i1fima2  24852  i1fd  24854  itg1addlem4  24872  itg1addlem4OLD  24873  dvidlem  25088  dvcnp  25092  dvadd  25113  dvmul  25114  dvaddf  25115  dvmulf  25116  dvco  25120  dvcof  25121  dvcjbr  25122  dvcj  25123  dvrec  25128  dvcnvlem  25149  dvef  25153  dvferm1  25158  dvferm2  25160  c1liplem1  25169  dvcnvrelem2  25191  mdegcl  25243  deg1n0ima  25263  plyco0  25362  plypf1  25382  tayl0  25530  ulmdvlem3  25570  pserdv  25597  dvlog  25815  efopn  25822  relogbf  25950  subusgr  27665  pthdivtx  28106  pthdlem2lem  28144  issh2  29580  hlimuni  29609  hhsscms  29649  occllem  29674  occl  29675  chscllem4  30011  imaelshi  30429  xrofsup  31099  tocyc01  31394  dimval  31695  dimvalfi  31696  smatrcl  31755  mdetpmtr1  31782  locfinreflem  31799  fsumcvg4  31909  zrhunitpreima  31937  imambfm  32238  carsggect  32294  sibfof  32316  eulerpartlemt  32347  eulerpartlemmf  32351  eulerpartlemgvv  32352  eulerpartlemgf  32355  rpsqrtcn  32582  cardpred  33071  nummin  33072  erdszelem2  33163  erdszelem7  33168  erdszelem8  33169  cvmliftlem15  33269  mrsub0  33487  mrsubccat  33489  mrsubcn  33490  mthmblem  33551  nofun  33861  madeval  34045  oldf  34050  oldlim  34078  ivthALT  34533  icoreunrn  35539  icoreelrn  35541  curf  35764  curunc  35768  heicant  35821  opnmbllem0  35822  mblfinlem1  35823  itg2addnclem  35837  itg2addnclem2  35838  ftc1anclem7  35865  ftc1anc  35867  ftc2nc  35868  indexdom  35901  cnres2  35930  elrfirn  40524  fnwe2lem2  40883  arearect  41053  areaquad  41054  absfun  42896  evthiccabs  43041  ioofun  43096  cncficcgt0  43436  fperdvper  43467  fvvolioof  43537  fvvolicof  43539  fourierdlem20  43675  fourierdlem42  43697  fourierdlem63  43717  fourierdlem76  43730  fourierdlem93  43747  fourierdlem97  43751  fourierdlem113  43767  ovolval3  44192  uniimafveqt  44844  fundcmpsurbijinjpreimafv  44870  fundcmpsurbijinj  44873  fundcmpsurinjALT  44875  fmtnoinf  44999  elbigolo1  45914