Theorem ffun 6490

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

Syntax hints:   → wi 4  Fun wfun 6318   Fn wfn 6319  ⟶wf 6320

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 210  df-an 400  df-fn 6327  df-f 6328

This theorem is referenced by:  ffund  6491  funssxp  6509  f00  6535  fimadmfoALT  6576  fimacnv  6816  dff3  6843  fliftf  7047  fiun  7626  f1iun  7627  frnsuppeq  7825  pmfun  8409  pmresg  8417  fodomr  8652  ac6sfi  8746  fissuni  8813  fipreima  8814  frnfsuppbi  8846  cnfcomlem  9146  tcrank  9297  fseqenlem2  9436  carduniima  9507  infmap2  9629  hsmexlem4  9840  hsmexlem5  9841  axdc3lem2  9862  axdc3lem4  9864  smobeth  9997  fpwwe2lem13  10053  inar1  10186  grur1  10231  nqerid  10344  zexALT  11989  hashkf  13688  hashgval  13689  revco  14187  ccatco  14188  pfxco  14191  lswco  14192  climdm  14903  isercolllem2  15014  isercolllem3  15015  isercoll  15016  sum0  15070  sumz  15071  fsumsers  15077  isumclim  15104  ntrivcvgfvn0  15247  ntrivcvgtail  15248  zprodn0  15285  iprodclim  15344  znnen  15557  isacs2  16916  isacs5  17774  dprdss  19144  dprd2dlem1  19156  dmdprdsplit2lem  19160  iscnp3  21849  subbascn  21859  cnpnei  21869  cnclima  21873  iscncl  21874  cncls  21879  cnrest2  21891  cnhaus  21959  kgencn3  22163  xkopt  22260  xkococnlem  22264  hmeores  22376  fbasrn  22489  uzrest  22502  rnelfmlem  22557  rnelfm  22558  fmfnfmlem3  22561  fmfnfmlem4  22562  fmfnfm  22563  cnflf2  22608  metcnp  23148  metustsym  23162  cfilucfil  23166  restmetu  23177  qtopbaslem  23364  tgqioo  23405  re2ndc  23406  bndth  23563  tcphcph  23841  ovolficcss  24073  volf  24133  volsup  24160  uniioombllem3a  24188  uniioombllem4  24190  uniioombllem5  24191  dyadmbllem  24203  dyadmbl  24204  opnmbllem  24205  opnmblALT  24207  mbfimaicc  24235  ismbf3d  24258  mbfimaopnlem  24259  mbfimaopn2  24261  i1fima  24282  i1fima2  24283  i1fd  24285  itg1addlem4  24303  dvidlem  24518  dvcnp  24522  dvadd  24543  dvmul  24544  dvaddf  24545  dvmulf  24546  dvco  24550  dvcof  24551  dvcjbr  24552  dvcj  24553  dvrec  24558  dvcnvlem  24579  dvef  24583  dvferm1  24588  dvferm2  24590  c1liplem1  24599  dvcnvrelem2  24621  mdegcl  24670  deg1n0ima  24690  plyco0  24789  plypf1  24809  tayl0  24957  ulmdvlem3  24997  pserdv  25024  dvlog  25242  efopn  25249  relogbf  25377  subusgr  27079  pthdivtx  27518  pthdlem2lem  27556  issh2  28992  hlimuni  29021  hhsscms  29061  occllem  29086  occl  29087  chscllem4  29423  imaelshi  29841  xrofsup  30518  tocyc01  30810  dimval  31089  dimvalfi  31090  smatrcl  31149  mdetpmtr1  31176  locfinreflem  31193  fsumcvg4  31303  zrhunitpreima  31329  imambfm  31630  carsggect  31686  sibfof  31708  eulerpartlemt  31739  eulerpartlemmf  31743  eulerpartlemgvv  31744  eulerpartlemgf  31747  rpsqrtcn  31974  cardpred  32473  nummin  32474  erdszelem2  32552  erdszelem7  32557  erdszelem8  32558  cvmliftlem15  32658  mrsub0  32876  mrsubccat  32878  mrsubcn  32879  mthmblem  32940  nofun  33269  madeval  33402  ivthALT  33796  icoreunrn  34776  icoreelrn  34778  curf  35035  curunc  35039  heicant  35092  opnmbllem0  35093  mblfinlem1  35094  itg2addnclem  35108  itg2addnclem2  35109  ftc1anclem7  35136  ftc1anc  35138  ftc2nc  35139  indexdom  35172  cnres2  35201  elrfirn  39636  fnwe2lem2  39995  arearect  40165  areaquad  40166  absfun  41982  evthiccabs  42133  ioofun  42188  cncficcgt0  42530  fperdvper  42561  fvvolioof  42631  fvvolicof  42633  fourierdlem20  42769  fourierdlem42  42791  fourierdlem63  42811  fourierdlem76  42824  fourierdlem93  42841  fourierdlem97  42845  fourierdlem113  42861  ovolval3  43286  uniimafveqt  43898  fundcmpsurbijinjpreimafv  43924  fundcmpsurbijinj  43927  fundcmpsurinjALT  43929  fmtnoinf  44053  elbigolo1  44971