Theorem ffun 6691

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

Syntax hints:   → wi 4  Fun wfun 6505   Fn wfn 6506  ⟶wf 6507

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 6514  df-f 6515

This theorem is referenced by:  ffund  6692  fco  6712  funssxp  6716  f00  6742  f1cof1  6766  fimadmfoALT  6783  dff3  7072  fliftf  7290  fiun  7921  f1iun  7922  fsuppeq  8154  fsuppeqg  8155  pmfun  8820  pmresg  8843  fodomr  9092  ac6sfi  9231  fodomfir  9279  fissuni  9308  fipreima  9309  ffsuppbi  9349  cnfcomlem  9652  tcrank  9837  fseqenlem2  9978  carduniima  10049  infmap2  10170  hsmexlem4  10382  hsmexlem5  10383  axdc3lem2  10404  axdc3lem4  10406  smobeth  10539  fpwwe2lem12  10595  inar1  10728  grur1  10773  nqerid  10886  fcdmnn0fsuppg  12502  zexALT  12549  hashkf  14297  hashgval  14298  revco  14800  ccatco  14801  pfxco  14804  lswco  14805  climdm  15520  isercolllem2  15632  isercolllem3  15633  isercoll  15634  sum0  15687  sumz  15688  fsumsers  15694  isumclim  15723  ntrivcvgfvn0  15865  ntrivcvgtail  15866  zprodn0  15905  iprodclim  15964  znnen  16180  isacs2  17614  isacs5  18507  dprdss  19961  dprd2dlem1  19973  dmdprdsplit2lem  19977  iscnp3  23131  subbascn  23141  cnpnei  23151  cnclima  23155  iscncl  23156  cncls  23161  cnrest2  23173  cnhaus  23241  kgencn3  23445  xkopt  23542  xkococnlem  23546  hmeores  23658  fbasrn  23771  uzrest  23784  rnelfmlem  23839  rnelfm  23840  fmfnfmlem3  23843  fmfnfmlem4  23844  fmfnfm  23845  cnflf2  23890  metcnp  24429  metustsym  24443  cfilucfil  24447  restmetu  24458  qtopbaslem  24646  tgqioo  24688  re2ndc  24689  bndth  24857  tcphcph  25137  ovolficcss  25370  volf  25430  volsup  25457  uniioombllem3a  25485  uniioombllem4  25487  uniioombllem5  25488  dyadmbllem  25500  dyadmbl  25501  opnmbllem  25502  opnmblALT  25504  mbfimaicc  25532  ismbf3d  25555  mbfimaopnlem  25556  mbfimaopn2  25558  i1fima  25579  i1fima2  25580  i1fd  25582  itg1addlem4  25600  dvidlem  25816  dvcnp  25820  dvadd  25843  dvmul  25844  dvaddf  25845  dvmulf  25846  dvco  25851  dvcof  25852  dvcjbr  25853  dvcj  25854  dvrec  25859  dvcnvlem  25880  dvef  25884  dvferm1  25889  dvferm2  25891  c1liplem1  25901  dvcnvrelem2  25923  mdegcl  25974  deg1n0ima  25994  plyco0  26097  plypf1  26117  tayl0  26269  ulmdvlem3  26311  pserdv  26339  dvlog  26560  efopn  26567  relogbf  26701  nofun  27561  madeval  27760  oldf  27765  oldlim  27798  madefi  27824  oldfi  27825  subusgr  29216  pthdivtx  29657  pthdlem2lem  29697  cyclnumvtx  29730  issh2  31138  hlimuni  31167  hhsscms  31207  occllem  31232  occl  31233  chscllem4  31569  imaelshi  31987  xrofsup  32690  tocyc01  33075  exsslsb  33592  dimval  33596  dimvalfi  33597  smatrcl  33786  mdetpmtr1  33813  locfinreflem  33830  fsumcvg4  33940  zrhunitpreima  33966  imambfm  34253  carsggect  34309  sibfof  34331  eulerpartlemt  34362  eulerpartlemmf  34366  eulerpartlemgvv  34367  eulerpartlemgf  34370  rpsqrtcn  34584  cardpred  35080  nummin  35081  erdszelem2  35179  erdszelem7  35184  erdszelem8  35185  cvmliftlem15  35285  mrsub0  35503  mrsubccat  35505  mrsubcn  35506  mthmblem  35567  ivthALT  36323  icoreunrn  37347  icoreelrn  37349  curf  37592  curunc  37596  heicant  37649  opnmbllem0  37650  mblfinlem1  37651  itg2addnclem  37665  itg2addnclem2  37666  ftc1anclem7  37693  ftc1anc  37695  ftc2nc  37696  indexdom  37728  cnres2  37757  aks6d1c6lem2  42159  elrfirn  42683  fnwe2lem2  43040  arearect  43204  areaquad  43205  naddcnff  43351  dfno2  43417  relpfr  44944  absfun  45346  evthiccabs  45494  ioofun  45549  cncficcgt0  45886  fperdvper  45917  fvvolioof  45987  fvvolicof  45989  fourierdlem20  46125  fourierdlem42  46147  fourierdlem63  46167  fourierdlem76  46180  fourierdlem93  46197  fourierdlem97  46201  fourierdlem113  46217  ovolval3  46645  tannpoly  46891  sinnpoly  46892  uniimafveqt  47382  fundcmpsurbijinjpreimafv  47408  fundcmpsurbijinj  47411  fundcmpsurinjALT  47413  fmtnoinf  47537  isubgruhgr  47868  upgrimwlklem1  47897  elbigolo1  48546