Theorem ffun 6665

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

Syntax hints:   → wi 4  Fun wfun 6486   Fn wfn 6487  ⟶wf 6488

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 6495  df-f 6496

This theorem is referenced by:  ffund  6666  fco  6686  funssxp  6690  f00  6716  f1cof1  6740  fimadmfoALT  6757  dff3  7046  fliftf  7263  fiun  7889  f1iun  7890  fsuppeq  8118  fsuppeqg  8119  pmfun  8787  pmresg  8811  fodomr  9059  ac6sfi  9187  fodomfir  9231  fissuni  9260  fipreima  9261  ffsuppbi  9304  cnfcomlem  9611  tcrank  9799  fseqenlem2  9938  carduniima  10009  infmap2  10130  hsmexlem4  10342  hsmexlem5  10343  axdc3lem2  10364  axdc3lem4  10366  smobeth  10500  fpwwe2lem12  10556  inar1  10689  grur1  10734  nqerid  10847  fcdmnn0fsuppg  12488  zexALT  12535  hashkf  14285  hashgval  14286  revco  14787  ccatco  14788  pfxco  14791  lswco  14792  climdm  15507  isercolllem2  15619  isercolllem3  15620  isercoll  15621  sum0  15674  sumz  15675  fsumsers  15681  isumclim  15710  ntrivcvgfvn0  15855  ntrivcvgtail  15856  zprodn0  15895  iprodclim  15954  znnen  16170  isacs2  17610  isacs5  18505  dprdss  19997  dprd2dlem1  20009  dmdprdsplit2lem  20013  iscnp3  23219  subbascn  23229  cnpnei  23239  cnclima  23243  iscncl  23244  cncls  23249  cnrest2  23261  cnhaus  23329  kgencn3  23533  xkopt  23630  xkococnlem  23634  hmeores  23746  fbasrn  23859  uzrest  23872  rnelfmlem  23927  rnelfm  23928  fmfnfmlem3  23931  fmfnfmlem4  23932  fmfnfm  23933  cnflf2  23978  metcnp  24516  metustsym  24530  cfilucfil  24534  restmetu  24545  qtopbaslem  24733  tgqioo  24775  re2ndc  24776  bndth  24935  tcphcph  25214  ovolficcss  25446  volf  25506  volsup  25533  uniioombllem3a  25561  uniioombllem4  25563  uniioombllem5  25564  dyadmbllem  25576  dyadmbl  25577  opnmbllem  25578  opnmblALT  25580  mbfimaicc  25608  ismbf3d  25631  mbfimaopnlem  25632  mbfimaopn2  25634  i1fima  25655  i1fima2  25656  i1fd  25658  itg1addlem4  25676  dvidlem  25892  dvcnp  25896  dvadd  25917  dvmul  25918  dvaddf  25919  dvmulf  25920  dvco  25924  dvcof  25925  dvcjbr  25926  dvcj  25927  dvrec  25932  dvcnvlem  25953  dvef  25957  dvferm1  25962  dvferm2  25964  c1liplem1  25973  dvcnvrelem2  25995  mdegcl  26044  deg1n0ima  26064  plyco0  26167  plypf1  26187  tayl0  26338  ulmdvlem3  26380  pserdv  26407  dvlog  26628  efopn  26635  relogbf  26768  nofun  27627  madeval  27838  oldf  27843  oldlim  27893  madefi  27919  oldfi  27920  oldfib  28383  subusgr  29372  pthdivtx  29810  pthdlem2lem  29850  cyclnumvtx  29883  issh2  31295  hlimuni  31324  hhsscms  31364  occllem  31389  occl  31390  chscllem4  31726  imaelshi  32144  xrofsup  32855  tocyc01  33194  exsslsb  33756  dimval  33760  dimvalfi  33761  smatrcl  33956  mdetpmtr1  33983  locfinreflem  34000  fsumcvg4  34110  zrhunitpreima  34136  imambfm  34422  carsggect  34478  sibfof  34500  eulerpartlemt  34531  eulerpartlemmf  34535  eulerpartlemgvv  34536  eulerpartlemgf  34539  rpsqrtcn  34753  cardpred  35251  nummin  35252  erdszelem2  35390  erdszelem7  35395  erdszelem8  35396  cvmliftlem15  35496  mrsub0  35714  mrsubccat  35716  mrsubcn  35717  mthmblem  35778  ivthALT  36533  icoreunrn  37689  icoreelrn  37691  curf  37933  curunc  37937  heicant  37990  opnmbllem0  37991  mblfinlem1  37992  itg2addnclem  38006  itg2addnclem2  38007  ftc1anclem7  38034  ftc1anc  38036  ftc2nc  38037  indexdom  38069  cnres2  38098  aks6d1c6lem2  42624  elrfirn  43141  fnwe2lem2  43497  arearect  43661  areaquad  43662  naddcnff  43808  dfno2  43873  relpfr  45399  absfun  45798  evthiccabs  45944  ioofun  45999  cncficcgt0  46334  fperdvper  46365  fvvolioof  46435  fvvolicof  46437  fourierdlem20  46573  fourierdlem42  46595  fourierdlem63  46615  fourierdlem76  46628  fourierdlem93  46645  fourierdlem97  46649  fourierdlem113  46665  ovolval3  47093  tannpoly  47350  sinnpoly  47351  uniimafveqt  47853  fundcmpsurbijinjpreimafv  47879  fundcmpsurbijinj  47882  fundcmpsurinjALT  47884  fmtnoinf  48011  isubgruhgr  48356  upgrimwlklem1  48385  elbigolo1  49045