Theorem ffun 6517

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

Syntax hints:   → wi 4  Fun wfun 6349   Fn wfn 6350  ⟶wf 6351

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 6358  df-f 6359

This theorem is referenced by:  ffund  6518  funssxp  6535  f00  6561  fimadmfoALT  6601  fimacnv  6839  dff3  6866  fliftf  7068  fiun  7644  f1iun  7645  frnsuppeq  7842  pmfun  8426  pmresg  8434  fodomr  8668  ac6sfi  8762  fissuni  8829  fipreima  8830  frnfsuppbi  8862  cnfcomlem  9162  tcrank  9313  fseqenlem2  9451  carduniima  9522  infmap2  9640  hsmexlem4  9851  hsmexlem5  9852  axdc3lem2  9873  axdc3lem4  9875  smobeth  10008  fpwwe2lem13  10064  inar1  10197  grur1  10242  nqerid  10355  zexALT  12002  hashkf  13693  hashgval  13694  revco  14196  ccatco  14197  pfxco  14200  lswco  14201  climdm  14911  isercolllem2  15022  isercolllem3  15023  isercoll  15024  sum0  15078  sumz  15079  fsumsers  15085  isumclim  15112  ntrivcvgfvn0  15255  ntrivcvgtail  15256  zprodn0  15293  iprodclim  15352  znnen  15565  isacs2  16924  isacs5  17782  dprdss  19151  dprd2dlem1  19163  dmdprdsplit2lem  19167  iscnp3  21852  subbascn  21862  cnpnei  21872  cnclima  21876  iscncl  21877  cncls  21882  cnrest2  21894  cnhaus  21962  kgencn3  22166  xkopt  22263  xkococnlem  22267  hmeores  22379  fbasrn  22492  uzrest  22505  rnelfmlem  22560  rnelfm  22561  fmfnfmlem3  22564  fmfnfmlem4  22565  fmfnfm  22566  cnflf2  22611  metcnp  23151  metustsym  23165  cfilucfil  23169  restmetu  23180  qtopbaslem  23367  tgqioo  23408  re2ndc  23409  bndth  23562  tcphcph  23840  ovolficcss  24070  volf  24130  volsup  24157  uniioombllem3a  24185  uniioombllem4  24187  uniioombllem5  24188  dyadmbllem  24200  dyadmbl  24201  opnmbllem  24202  opnmblALT  24204  mbfimaicc  24232  ismbf3d  24255  mbfimaopnlem  24256  mbfimaopn2  24258  i1fima  24279  i1fima2  24280  i1fd  24282  itg1addlem4  24300  dvidlem  24513  dvcnp  24516  dvadd  24537  dvmul  24538  dvaddf  24539  dvmulf  24540  dvco  24544  dvcof  24545  dvcjbr  24546  dvcj  24547  dvrec  24552  dvcnvlem  24573  dvef  24577  dvferm1  24582  dvferm2  24584  c1liplem1  24593  dvcnvrelem2  24615  mdegcl  24663  deg1n0ima  24683  plyco0  24782  plypf1  24802  tayl0  24950  ulmdvlem3  24990  pserdv  25017  dvlog  25234  efopn  25241  relogbf  25369  subusgr  27071  pthdivtx  27510  pthdlem2lem  27548  issh2  28986  hlimuni  29015  hhsscms  29055  occllem  29080  occl  29081  chscllem4  29417  imaelshi  29835  xrofsup  30492  tocyc01  30760  dimval  31001  dimvalfi  31002  smatrcl  31061  mdetpmtr1  31088  locfinreflem  31104  fsumcvg4  31193  zrhunitpreima  31219  imambfm  31520  carsggect  31576  sibfof  31598  eulerpartlemt  31629  eulerpartlemmf  31633  eulerpartlemgvv  31634  eulerpartlemgf  31637  rpsqrtcn  31864  erdszelem2  32439  erdszelem7  32444  erdszelem8  32445  cvmliftlem15  32545  mrsub0  32763  mrsubccat  32765  mrsubcn  32766  mthmblem  32827  nofun  33156  madeval  33289  ivthALT  33683  icoreunrn  34643  icoreelrn  34645  curf  34885  curunc  34889  heicant  34942  opnmbllem0  34943  mblfinlem1  34944  itg2addnclem  34958  itg2addnclem2  34959  ftc1anclem7  34988  ftc1anc  34990  ftc2nc  34991  indexdom  35024  cnres2  35056  elrfirn  39341  fnwe2lem2  39700  arearect  39871  areaquad  39872  absfun  41667  evthiccabs  41820  ioofun  41876  cncficcgt0  42220  fperdvper  42252  fvvolioof  42323  fvvolicof  42325  fourierdlem20  42461  fourierdlem42  42483  fourierdlem63  42503  fourierdlem76  42516  fourierdlem93  42533  fourierdlem97  42537  fourierdlem113  42553  ovolval3  42978  uniimafveqt  43590  fundcmpsurbijinjpreimafv  43616  fundcmpsurbijinj  43619  fundcmpsurinjALT  43621  fmtnoinf  43747  elbigolo1  44666