Theorem ffun 6709

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

Syntax hints:   → wi 4  Fun wfun 6525   Fn wfn 6526  ⟶wf 6527

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 6534  df-f 6535

This theorem is referenced by:  ffund  6710  fco  6730  funssxp  6734  f00  6760  f1cof1  6784  fimadmfoALT  6801  dff3  7090  fliftf  7308  fiun  7941  f1iun  7942  fsuppeq  8174  fsuppeqg  8175  pmfun  8861  pmresg  8884  fodomr  9142  ac6sfi  9292  fodomfir  9340  fissuni  9369  fipreima  9370  ffsuppbi  9410  cnfcomlem  9713  tcrank  9898  fseqenlem2  10039  carduniima  10110  infmap2  10231  hsmexlem4  10443  hsmexlem5  10444  axdc3lem2  10465  axdc3lem4  10467  smobeth  10600  fpwwe2lem12  10656  inar1  10789  grur1  10834  nqerid  10947  fcdmnn0fsuppg  12561  zexALT  12608  hashkf  14350  hashgval  14351  revco  14853  ccatco  14854  pfxco  14857  lswco  14858  climdm  15570  isercolllem2  15682  isercolllem3  15683  isercoll  15684  sum0  15737  sumz  15738  fsumsers  15744  isumclim  15773  ntrivcvgfvn0  15915  ntrivcvgtail  15916  zprodn0  15955  iprodclim  16014  znnen  16230  isacs2  17665  isacs5  18558  dprdss  20012  dprd2dlem1  20024  dmdprdsplit2lem  20028  iscnp3  23182  subbascn  23192  cnpnei  23202  cnclima  23206  iscncl  23207  cncls  23212  cnrest2  23224  cnhaus  23292  kgencn3  23496  xkopt  23593  xkococnlem  23597  hmeores  23709  fbasrn  23822  uzrest  23835  rnelfmlem  23890  rnelfm  23891  fmfnfmlem3  23894  fmfnfmlem4  23895  fmfnfm  23896  cnflf2  23941  metcnp  24480  metustsym  24494  cfilucfil  24498  restmetu  24509  qtopbaslem  24697  tgqioo  24739  re2ndc  24740  bndth  24908  tcphcph  25189  ovolficcss  25422  volf  25482  volsup  25509  uniioombllem3a  25537  uniioombllem4  25539  uniioombllem5  25540  dyadmbllem  25552  dyadmbl  25553  opnmbllem  25554  opnmblALT  25556  mbfimaicc  25584  ismbf3d  25607  mbfimaopnlem  25608  mbfimaopn2  25610  i1fima  25631  i1fima2  25632  i1fd  25634  itg1addlem4  25652  dvidlem  25868  dvcnp  25872  dvadd  25895  dvmul  25896  dvaddf  25897  dvmulf  25898  dvco  25903  dvcof  25904  dvcjbr  25905  dvcj  25906  dvrec  25911  dvcnvlem  25932  dvef  25936  dvferm1  25941  dvferm2  25943  c1liplem1  25953  dvcnvrelem2  25975  mdegcl  26026  deg1n0ima  26046  plyco0  26149  plypf1  26169  tayl0  26321  ulmdvlem3  26363  pserdv  26391  dvlog  26612  efopn  26619  relogbf  26753  nofun  27613  madeval  27812  oldf  27817  oldlim  27850  madefi  27876  oldfi  27877  subusgr  29268  pthdivtx  29709  pthdlem2lem  29749  cyclnumvtx  29782  issh2  31190  hlimuni  31219  hhsscms  31259  occllem  31284  occl  31285  chscllem4  31621  imaelshi  32039  xrofsup  32744  tocyc01  33129  exsslsb  33636  dimval  33640  dimvalfi  33641  smatrcl  33827  mdetpmtr1  33854  locfinreflem  33871  fsumcvg4  33981  zrhunitpreima  34007  imambfm  34294  carsggect  34350  sibfof  34372  eulerpartlemt  34403  eulerpartlemmf  34407  eulerpartlemgvv  34408  eulerpartlemgf  34411  rpsqrtcn  34625  cardpred  35121  nummin  35122  erdszelem2  35214  erdszelem7  35219  erdszelem8  35220  cvmliftlem15  35320  mrsub0  35538  mrsubccat  35540  mrsubcn  35541  mthmblem  35602  ivthALT  36353  icoreunrn  37377  icoreelrn  37379  curf  37622  curunc  37626  heicant  37679  opnmbllem0  37680  mblfinlem1  37681  itg2addnclem  37695  itg2addnclem2  37696  ftc1anclem7  37723  ftc1anc  37725  ftc2nc  37726  indexdom  37758  cnres2  37787  aks6d1c6lem2  42184  elrfirn  42718  fnwe2lem2  43075  arearect  43239  areaquad  43240  naddcnff  43386  dfno2  43452  relpfr  44979  absfun  45377  evthiccabs  45525  ioofun  45580  cncficcgt0  45917  fperdvper  45948  fvvolioof  46018  fvvolicof  46020  fourierdlem20  46156  fourierdlem42  46178  fourierdlem63  46198  fourierdlem76  46211  fourierdlem93  46228  fourierdlem97  46232  fourierdlem113  46248  ovolval3  46676  uniimafveqt  47395  fundcmpsurbijinjpreimafv  47421  fundcmpsurbijinj  47424  fundcmpsurinjALT  47426  fmtnoinf  47550  isubgruhgr  47881  upgrimwlklem1  47910  elbigolo1  48537