Theorem ffun 6665

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

Syntax hints:   → wi 4  Fun wfun 6486   Fn wfn 6487  ⟶wf 6488

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 208  df-an 397  df-fn 6495  df-f 6496

This theorem is referenced by:  ffund  6666  fco  6686  funssxp  6690  f00  6716  f1cof1  6740  fimadmfoALT  6757  dff3  7048  fliftf  7266  fiun  7892  f1iun  7893  fsuppeq  8122  fsuppeqg  8123  pmfun  8791  pmresg  8815  fodomr  9063  ac6sfi  9191  fodomfir  9235  fissuni  9264  fipreima  9265  ffsuppbi  9308  cnfcomlem  9618  tcrank  9806  fseqenlem2  9945  carduniima  10016  infmap2  10137  hsmexlem4  10349  hsmexlem5  10350  axdc3lem2  10371  axdc3lem4  10373  smobeth  10507  fpwwe2lem12  10563  inar1  10696  grur1  10741  nqerid  10854  fcdmnn0fsuppg  12495  zexALT  12542  hashkf  14292  hashgval  14293  revco  14794  ccatco  14795  pfxco  14798  lswco  14799  climdm  15514  isercolllem2  15626  isercolllem3  15627  isercoll  15628  sum0  15681  sumz  15682  fsumsers  15688  isumclim  15717  ntrivcvgfvn0  15862  ntrivcvgtail  15863  zprodn0  15902  iprodclim  15961  znnen  16177  isacs2  17617  isacs5  18512  dprdss  20004  dprd2dlem1  20016  dmdprdsplit2lem  20020  iscnp3  23234  subbascn  23244  cnpnei  23254  cnclima  23258  iscncl  23259  cncls  23264  cnrest2  23276  cnhaus  23344  kgencn3  23548  xkopt  23645  xkococnlem  23649  hmeores  23761  fbasrn  23874  uzrest  23887  rnelfmlem  23942  rnelfm  23943  fmfnfmlem3  23946  fmfnfmlem4  23947  fmfnfm  23948  cnflf2  23993  metcnp  24531  metustsym  24545  cfilucfil  24549  restmetu  24560  qtopbaslem  24748  tgqioo  24790  re2ndc  24791  bndth  24950  tcphcph  25229  ovolficcss  25461  volf  25521  volsup  25548  uniioombllem3a  25576  uniioombllem4  25578  uniioombllem5  25579  dyadmbllem  25591  dyadmbl  25592  opnmbllem  25593  opnmblALT  25595  mbfimaicc  25623  ismbf3d  25646  mbfimaopnlem  25647  mbfimaopn2  25649  i1fima  25670  i1fima2  25671  i1fd  25673  itg1addlem4  25691  dvidlem  25907  dvcnp  25911  dvadd  25932  dvmul  25933  dvaddf  25934  dvmulf  25935  dvco  25939  dvcof  25940  dvcjbr  25941  dvcj  25942  dvrec  25947  dvcnvlem  25968  dvef  25972  dvferm1  25977  dvferm2  25979  c1liplem1  25988  dvcnvrelem2  26010  mdegcl  26059  deg1n0ima  26079  plyco0  26182  plypf1  26202  tayl0  26352  ulmdvlem3  26392  pserdv  26419  dvlog  26640  efopn  26647  relogbf  26780  nofun  27638  madeval  27849  oldf  27854  oldlim  27904  madefi  27930  oldfi  27931  oldfib  28394  subusgr  29383  pthdivtx  29820  pthdlem2lem  29860  cyclnumvtx  29893  issh2  31305  hlimuni  31334  hhsscms  31374  occllem  31399  occl  31400  chscllem4  31736  imaelshi  32154  xrofsup  32866  tocyc01  33206  exsslsb  33788  dimval  33792  dimvalfi  33793  smatrcl  33987  mdetpmtr1  34014  locfinreflem  34031  fsumcvg4  34141  zrhunitpreima  34167  imambfm  34453  carsggect  34509  sibfof  34531  eulerpartlemt  34562  eulerpartlemmf  34566  eulerpartlemgvv  34567  eulerpartlemgf  34570  rpsqrtcn  34784  cardpred  35280  nummin  35281  erdszelem2  35427  erdszelem7  35432  erdszelem8  35433  cvmliftlem15  35533  mrsub0  35751  mrsubccat  35753  mrsubcn  35754  mthmblem  35815  ivthALT  36570  icoreunrn  37728  icoreelrn  37730  curf  37972  curunc  37976  heicant  38029  opnmbllem0  38030  mblfinlem1  38031  itg2addnclem  38045  itg2addnclem2  38046  ftc1anclem7  38073  ftc1anc  38075  ftc2nc  38076  indexdom  38108  cnres2  38137  aks6d1c6lem2  42663  elrfirn  43151  fnwe2lem2  43503  arearect  43667  areaquad  43668  naddcnff  43814  dfno2  43879  relpfr  45405  absfun  45802  evthiccabs  45948  ioofun  46003  cncficcgt0  46338  fperdvper  46369  fvvolioof  46439  fvvolicof  46441  fourierdlem20  46577  fourierdlem42  46599  fourierdlem63  46619  fourierdlem76  46632  fourierdlem93  46649  fourierdlem97  46653  fourierdlem113  46669  ovolval3  47097  tannpoly  47360  sinnpoly  47361  uniimafveqt  47863  fundcmpsurbijinjpreimafv  47889  fundcmpsurbijinj  47892  fundcmpsurinjALT  47894  fmtnoinf  48021  isubgruhgr  48366  upgrimwlklem1  48395  elbigolo1  49055