Theorem ffun 6671

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

Syntax hints:   → wi 4  Fun wfun 6492   Fn wfn 6493  ⟶wf 6494

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 6501  df-f 6502

This theorem is referenced by:  ffund  6672  fco  6692  funssxp  6696  f00  6722  f1cof1  6746  fimadmfoALT  6763  dff3  7052  fliftf  7270  fiun  7896  f1iun  7897  fsuppeq  8125  fsuppeqg  8126  pmfun  8794  pmresg  8818  fodomr  9066  ac6sfi  9194  fodomfir  9238  fissuni  9267  fipreima  9268  ffsuppbi  9311  cnfcomlem  9620  tcrank  9808  fseqenlem2  9947  carduniima  10018  infmap2  10139  hsmexlem4  10351  hsmexlem5  10352  axdc3lem2  10373  axdc3lem4  10375  smobeth  10509  fpwwe2lem12  10565  inar1  10698  grur1  10743  nqerid  10856  fcdmnn0fsuppg  12497  zexALT  12544  hashkf  14294  hashgval  14295  revco  14796  ccatco  14797  pfxco  14800  lswco  14801  climdm  15516  isercolllem2  15628  isercolllem3  15629  isercoll  15630  sum0  15683  sumz  15684  fsumsers  15690  isumclim  15719  ntrivcvgfvn0  15864  ntrivcvgtail  15865  zprodn0  15904  iprodclim  15963  znnen  16179  isacs2  17619  isacs5  18514  dprdss  20006  dprd2dlem1  20018  dmdprdsplit2lem  20022  iscnp3  23209  subbascn  23219  cnpnei  23229  cnclima  23233  iscncl  23234  cncls  23239  cnrest2  23251  cnhaus  23319  kgencn3  23523  xkopt  23620  xkococnlem  23624  hmeores  23736  fbasrn  23849  uzrest  23862  rnelfmlem  23917  rnelfm  23918  fmfnfmlem3  23921  fmfnfmlem4  23922  fmfnfm  23923  cnflf2  23968  metcnp  24506  metustsym  24520  cfilucfil  24524  restmetu  24535  qtopbaslem  24723  tgqioo  24765  re2ndc  24766  bndth  24925  tcphcph  25204  ovolficcss  25436  volf  25496  volsup  25523  uniioombllem3a  25551  uniioombllem4  25553  uniioombllem5  25554  dyadmbllem  25566  dyadmbl  25567  opnmbllem  25568  opnmblALT  25570  mbfimaicc  25598  ismbf3d  25621  mbfimaopnlem  25622  mbfimaopn2  25624  i1fima  25645  i1fima2  25646  i1fd  25648  itg1addlem4  25666  dvidlem  25882  dvcnp  25886  dvadd  25907  dvmul  25908  dvaddf  25909  dvmulf  25910  dvco  25914  dvcof  25915  dvcjbr  25916  dvcj  25917  dvrec  25922  dvcnvlem  25943  dvef  25947  dvferm1  25952  dvferm2  25954  c1liplem1  25963  dvcnvrelem2  25985  mdegcl  26034  deg1n0ima  26054  plyco0  26157  plypf1  26177  tayl0  26327  ulmdvlem3  26367  pserdv  26394  dvlog  26615  efopn  26622  relogbf  26755  nofun  27613  madeval  27824  oldf  27829  oldlim  27879  madefi  27905  oldfi  27906  oldfib  28369  subusgr  29358  pthdivtx  29795  pthdlem2lem  29835  cyclnumvtx  29868  issh2  31280  hlimuni  31309  hhsscms  31349  occllem  31374  occl  31375  chscllem4  31711  imaelshi  32129  xrofsup  32840  tocyc01  33179  exsslsb  33741  dimval  33745  dimvalfi  33746  smatrcl  33940  mdetpmtr1  33967  locfinreflem  33984  fsumcvg4  34094  zrhunitpreima  34120  imambfm  34406  carsggect  34462  sibfof  34484  eulerpartlemt  34515  eulerpartlemmf  34519  eulerpartlemgvv  34520  eulerpartlemgf  34523  rpsqrtcn  34737  cardpred  35235  nummin  35236  erdszelem2  35374  erdszelem7  35379  erdszelem8  35380  cvmliftlem15  35480  mrsub0  35698  mrsubccat  35700  mrsubcn  35701  mthmblem  35762  ivthALT  36517  icoreunrn  37675  icoreelrn  37677  curf  37919  curunc  37923  heicant  37976  opnmbllem0  37977  mblfinlem1  37978  itg2addnclem  37992  itg2addnclem2  37993  ftc1anclem7  38020  ftc1anc  38022  ftc2nc  38023  indexdom  38055  cnres2  38084  aks6d1c6lem2  42610  elrfirn  43127  fnwe2lem2  43479  arearect  43643  areaquad  43644  naddcnff  43790  dfno2  43855  relpfr  45381  absfun  45780  evthiccabs  45926  ioofun  45981  cncficcgt0  46316  fperdvper  46347  fvvolioof  46417  fvvolicof  46419  fourierdlem20  46555  fourierdlem42  46577  fourierdlem63  46597  fourierdlem76  46610  fourierdlem93  46627  fourierdlem97  46631  fourierdlem113  46647  ovolval3  47075  tannpoly  47338  sinnpoly  47339  uniimafveqt  47841  fundcmpsurbijinjpreimafv  47867  fundcmpsurbijinj  47870  fundcmpsurinjALT  47872  fmtnoinf  47999  isubgruhgr  48344  upgrimwlklem1  48373  elbigolo1  49033