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 207  df-an 396  df-fn 6495  df-f 6496

This theorem is referenced by:  ffund  6666  fco  6686  funssxp  6690  f00  6716  f1cof1  6740  fimadmfoALT  6757  dff3  7045  fliftf  7261  fiun  7887  f1iun  7888  fsuppeq  8117  fsuppeqg  8118  pmfun  8784  pmresg  8808  fodomr  9056  ac6sfi  9184  fodomfir  9228  fissuni  9257  fipreima  9258  ffsuppbi  9301  cnfcomlem  9608  tcrank  9796  fseqenlem2  9935  carduniima  10006  infmap2  10127  hsmexlem4  10339  hsmexlem5  10340  axdc3lem2  10361  axdc3lem4  10363  smobeth  10497  fpwwe2lem12  10553  inar1  10686  grur1  10731  nqerid  10844  fcdmnn0fsuppg  12461  zexALT  12508  hashkf  14255  hashgval  14256  revco  14757  ccatco  14758  pfxco  14761  lswco  14762  climdm  15477  isercolllem2  15589  isercolllem3  15590  isercoll  15591  sum0  15644  sumz  15645  fsumsers  15651  isumclim  15680  ntrivcvgfvn0  15822  ntrivcvgtail  15823  zprodn0  15862  iprodclim  15921  znnen  16137  isacs2  17576  isacs5  18471  dprdss  19960  dprd2dlem1  19972  dmdprdsplit2lem  19976  iscnp3  23188  subbascn  23198  cnpnei  23208  cnclima  23212  iscncl  23213  cncls  23218  cnrest2  23230  cnhaus  23298  kgencn3  23502  xkopt  23599  xkococnlem  23603  hmeores  23715  fbasrn  23828  uzrest  23841  rnelfmlem  23896  rnelfm  23897  fmfnfmlem3  23900  fmfnfmlem4  23901  fmfnfm  23902  cnflf2  23947  metcnp  24485  metustsym  24499  cfilucfil  24503  restmetu  24514  qtopbaslem  24702  tgqioo  24744  re2ndc  24745  bndth  24913  tcphcph  25193  ovolficcss  25426  volf  25486  volsup  25513  uniioombllem3a  25541  uniioombllem4  25543  uniioombllem5  25544  dyadmbllem  25556  dyadmbl  25557  opnmbllem  25558  opnmblALT  25560  mbfimaicc  25588  ismbf3d  25611  mbfimaopnlem  25612  mbfimaopn2  25614  i1fima  25635  i1fima2  25636  i1fd  25638  itg1addlem4  25656  dvidlem  25872  dvcnp  25876  dvadd  25899  dvmul  25900  dvaddf  25901  dvmulf  25902  dvco  25907  dvcof  25908  dvcjbr  25909  dvcj  25910  dvrec  25915  dvcnvlem  25936  dvef  25940  dvferm1  25945  dvferm2  25947  c1liplem1  25957  dvcnvrelem2  25979  mdegcl  26030  deg1n0ima  26050  plyco0  26153  plypf1  26173  tayl0  26325  ulmdvlem3  26367  pserdv  26395  dvlog  26616  efopn  26623  relogbf  26757  nofun  27617  madeval  27828  oldf  27833  oldlim  27883  madefi  27909  oldfi  27910  oldfib  28373  subusgr  29362  pthdivtx  29800  pthdlem2lem  29840  cyclnumvtx  29873  issh2  31284  hlimuni  31313  hhsscms  31353  occllem  31378  occl  31379  chscllem4  31715  imaelshi  32133  xrofsup  32847  tocyc01  33200  exsslsb  33753  dimval  33757  dimvalfi  33758  smatrcl  33953  mdetpmtr1  33980  locfinreflem  33997  fsumcvg4  34107  zrhunitpreima  34133  imambfm  34419  carsggect  34475  sibfof  34497  eulerpartlemt  34528  eulerpartlemmf  34532  eulerpartlemgvv  34533  eulerpartlemgf  34536  rpsqrtcn  34750  cardpred  35248  nummin  35249  erdszelem2  35386  erdszelem7  35391  erdszelem8  35392  cvmliftlem15  35492  mrsub0  35710  mrsubccat  35712  mrsubcn  35713  mthmblem  35774  ivthALT  36529  icoreunrn  37560  icoreelrn  37562  curf  37795  curunc  37799  heicant  37852  opnmbllem0  37853  mblfinlem1  37854  itg2addnclem  37868  itg2addnclem2  37869  ftc1anclem7  37896  ftc1anc  37898  ftc2nc  37899  indexdom  37931  cnres2  37960  aks6d1c6lem2  42421  elrfirn  42933  fnwe2lem2  43289  arearect  43453  areaquad  43454  naddcnff  43600  dfno2  43665  relpfr  45191  absfun  45591  evthiccabs  45738  ioofun  45793  cncficcgt0  46128  fperdvper  46159  fvvolioof  46229  fvvolicof  46231  fourierdlem20  46367  fourierdlem42  46389  fourierdlem63  46409  fourierdlem76  46422  fourierdlem93  46439  fourierdlem97  46443  fourierdlem113  46459  ovolval3  46887  tannpoly  47132  sinnpoly  47133  uniimafveqt  47623  fundcmpsurbijinjpreimafv  47649  fundcmpsurbijinj  47652  fundcmpsurinjALT  47654  fmtnoinf  47778  isubgruhgr  48110  upgrimwlklem1  48139  elbigolo1  48799