Theorem ffun 6739

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

Syntax hints:   → wi 4  Fun wfun 6555   Fn wfn 6556  ⟶wf 6557

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 6564  df-f 6565

This theorem is referenced by:  ffund  6740  fco  6760  funssxp  6764  f00  6790  f1cof1  6814  fimadmfoALT  6831  dff3  7120  fliftf  7335  fiun  7967  f1iun  7968  fsuppeq  8200  fsuppeqg  8201  pmfun  8887  pmresg  8910  fodomr  9168  ac6sfi  9320  fodomfir  9368  fissuni  9397  fipreima  9398  ffsuppbi  9438  cnfcomlem  9739  tcrank  9924  fseqenlem2  10065  carduniima  10136  infmap2  10257  hsmexlem4  10469  hsmexlem5  10470  axdc3lem2  10491  axdc3lem4  10493  smobeth  10626  fpwwe2lem12  10682  inar1  10815  grur1  10860  nqerid  10973  fcdmnn0fsuppg  12586  zexALT  12633  hashkf  14371  hashgval  14372  revco  14873  ccatco  14874  pfxco  14877  lswco  14878  climdm  15590  isercolllem2  15702  isercolllem3  15703  isercoll  15704  sum0  15757  sumz  15758  fsumsers  15764  isumclim  15793  ntrivcvgfvn0  15935  ntrivcvgtail  15936  zprodn0  15975  iprodclim  16034  znnen  16248  isacs2  17696  isacs5  18593  dprdss  20049  dprd2dlem1  20061  dmdprdsplit2lem  20065  iscnp3  23252  subbascn  23262  cnpnei  23272  cnclima  23276  iscncl  23277  cncls  23282  cnrest2  23294  cnhaus  23362  kgencn3  23566  xkopt  23663  xkococnlem  23667  hmeores  23779  fbasrn  23892  uzrest  23905  rnelfmlem  23960  rnelfm  23961  fmfnfmlem3  23964  fmfnfmlem4  23965  fmfnfm  23966  cnflf2  24011  metcnp  24554  metustsym  24568  cfilucfil  24572  restmetu  24583  qtopbaslem  24779  tgqioo  24821  re2ndc  24822  bndth  24990  tcphcph  25271  ovolficcss  25504  volf  25564  volsup  25591  uniioombllem3a  25619  uniioombllem4  25621  uniioombllem5  25622  dyadmbllem  25634  dyadmbl  25635  opnmbllem  25636  opnmblALT  25638  mbfimaicc  25666  ismbf3d  25689  mbfimaopnlem  25690  mbfimaopn2  25692  i1fima  25713  i1fima2  25714  i1fd  25716  itg1addlem4  25734  dvidlem  25950  dvcnp  25954  dvadd  25977  dvmul  25978  dvaddf  25979  dvmulf  25980  dvco  25985  dvcof  25986  dvcjbr  25987  dvcj  25988  dvrec  25993  dvcnvlem  26014  dvef  26018  dvferm1  26023  dvferm2  26025  c1liplem1  26035  dvcnvrelem2  26057  mdegcl  26108  deg1n0ima  26128  plyco0  26231  plypf1  26251  tayl0  26403  ulmdvlem3  26445  pserdv  26473  dvlog  26693  efopn  26700  relogbf  26834  nofun  27694  madeval  27891  oldf  27896  oldlim  27925  madefi  27950  oldfi  27951  subusgr  29306  pthdivtx  29747  pthdlem2lem  29787  cyclnumvtx  29820  issh2  31228  hlimuni  31257  hhsscms  31297  occllem  31322  occl  31323  chscllem4  31659  imaelshi  32077  xrofsup  32771  tocyc01  33138  exsslsb  33647  dimval  33651  dimvalfi  33652  smatrcl  33795  mdetpmtr1  33822  locfinreflem  33839  fsumcvg4  33949  zrhunitpreima  33977  imambfm  34264  carsggect  34320  sibfof  34342  eulerpartlemt  34373  eulerpartlemmf  34377  eulerpartlemgvv  34378  eulerpartlemgf  34381  rpsqrtcn  34608  cardpred  35104  nummin  35105  erdszelem2  35197  erdszelem7  35202  erdszelem8  35203  cvmliftlem15  35303  mrsub0  35521  mrsubccat  35523  mrsubcn  35524  mthmblem  35585  ivthALT  36336  icoreunrn  37360  icoreelrn  37362  curf  37605  curunc  37609  heicant  37662  opnmbllem0  37663  mblfinlem1  37664  itg2addnclem  37678  itg2addnclem2  37679  ftc1anclem7  37706  ftc1anc  37708  ftc2nc  37709  indexdom  37741  cnres2  37770  aks6d1c6lem2  42172  elrfirn  42706  fnwe2lem2  43063  arearect  43227  areaquad  43228  naddcnff  43375  dfno2  43441  relpfr  44975  absfun  45361  evthiccabs  45509  ioofun  45564  cncficcgt0  45903  fperdvper  45934  fvvolioof  46004  fvvolicof  46006  fourierdlem20  46142  fourierdlem42  46164  fourierdlem63  46184  fourierdlem76  46197  fourierdlem93  46214  fourierdlem97  46218  fourierdlem113  46234  ovolval3  46662  uniimafveqt  47368  fundcmpsurbijinjpreimafv  47394  fundcmpsurbijinj  47397  fundcmpsurinjALT  47399  fmtnoinf  47523  isubgruhgr  47854  elbigolo1  48478