Theorem ffun 6694

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

Syntax hints:   → wi 4  Fun wfun 6508   Fn wfn 6509  ⟶wf 6510

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 6517  df-f 6518

This theorem is referenced by:  ffund  6695  fco  6715  funssxp  6719  f00  6745  f1cof1  6769  fimadmfoALT  6786  dff3  7075  fliftf  7293  fiun  7924  f1iun  7925  fsuppeq  8157  fsuppeqg  8158  pmfun  8823  pmresg  8846  fodomr  9098  ac6sfi  9238  fodomfir  9286  fissuni  9315  fipreima  9316  ffsuppbi  9356  cnfcomlem  9659  tcrank  9844  fseqenlem2  9985  carduniima  10056  infmap2  10177  hsmexlem4  10389  hsmexlem5  10390  axdc3lem2  10411  axdc3lem4  10413  smobeth  10546  fpwwe2lem12  10602  inar1  10735  grur1  10780  nqerid  10893  fcdmnn0fsuppg  12509  zexALT  12556  hashkf  14304  hashgval  14305  revco  14807  ccatco  14808  pfxco  14811  lswco  14812  climdm  15527  isercolllem2  15639  isercolllem3  15640  isercoll  15641  sum0  15694  sumz  15695  fsumsers  15701  isumclim  15730  ntrivcvgfvn0  15872  ntrivcvgtail  15873  zprodn0  15912  iprodclim  15971  znnen  16187  isacs2  17621  isacs5  18514  dprdss  19968  dprd2dlem1  19980  dmdprdsplit2lem  19984  iscnp3  23138  subbascn  23148  cnpnei  23158  cnclima  23162  iscncl  23163  cncls  23168  cnrest2  23180  cnhaus  23248  kgencn3  23452  xkopt  23549  xkococnlem  23553  hmeores  23665  fbasrn  23778  uzrest  23791  rnelfmlem  23846  rnelfm  23847  fmfnfmlem3  23850  fmfnfmlem4  23851  fmfnfm  23852  cnflf2  23897  metcnp  24436  metustsym  24450  cfilucfil  24454  restmetu  24465  qtopbaslem  24653  tgqioo  24695  re2ndc  24696  bndth  24864  tcphcph  25144  ovolficcss  25377  volf  25437  volsup  25464  uniioombllem3a  25492  uniioombllem4  25494  uniioombllem5  25495  dyadmbllem  25507  dyadmbl  25508  opnmbllem  25509  opnmblALT  25511  mbfimaicc  25539  ismbf3d  25562  mbfimaopnlem  25563  mbfimaopn2  25565  i1fima  25586  i1fima2  25587  i1fd  25589  itg1addlem4  25607  dvidlem  25823  dvcnp  25827  dvadd  25850  dvmul  25851  dvaddf  25852  dvmulf  25853  dvco  25858  dvcof  25859  dvcjbr  25860  dvcj  25861  dvrec  25866  dvcnvlem  25887  dvef  25891  dvferm1  25896  dvferm2  25898  c1liplem1  25908  dvcnvrelem2  25930  mdegcl  25981  deg1n0ima  26001  plyco0  26104  plypf1  26124  tayl0  26276  ulmdvlem3  26318  pserdv  26346  dvlog  26567  efopn  26574  relogbf  26708  nofun  27568  madeval  27767  oldf  27772  oldlim  27805  madefi  27831  oldfi  27832  subusgr  29223  pthdivtx  29664  pthdlem2lem  29704  cyclnumvtx  29737  issh2  31145  hlimuni  31174  hhsscms  31214  occllem  31239  occl  31240  chscllem4  31576  imaelshi  31994  xrofsup  32697  tocyc01  33082  exsslsb  33599  dimval  33603  dimvalfi  33604  smatrcl  33793  mdetpmtr1  33820  locfinreflem  33837  fsumcvg4  33947  zrhunitpreima  33973  imambfm  34260  carsggect  34316  sibfof  34338  eulerpartlemt  34369  eulerpartlemmf  34373  eulerpartlemgvv  34374  eulerpartlemgf  34377  rpsqrtcn  34591  cardpred  35087  nummin  35088  erdszelem2  35186  erdszelem7  35191  erdszelem8  35192  cvmliftlem15  35292  mrsub0  35510  mrsubccat  35512  mrsubcn  35513  mthmblem  35574  ivthALT  36330  icoreunrn  37354  icoreelrn  37356  curf  37599  curunc  37603  heicant  37656  opnmbllem0  37657  mblfinlem1  37658  itg2addnclem  37672  itg2addnclem2  37673  ftc1anclem7  37700  ftc1anc  37702  ftc2nc  37703  indexdom  37735  cnres2  37764  aks6d1c6lem2  42166  elrfirn  42690  fnwe2lem2  43047  arearect  43211  areaquad  43212  naddcnff  43358  dfno2  43424  relpfr  44951  absfun  45353  evthiccabs  45501  ioofun  45556  cncficcgt0  45893  fperdvper  45924  fvvolioof  45994  fvvolicof  45996  fourierdlem20  46132  fourierdlem42  46154  fourierdlem63  46174  fourierdlem76  46187  fourierdlem93  46204  fourierdlem97  46208  fourierdlem113  46224  ovolval3  46652  uniimafveqt  47386  fundcmpsurbijinjpreimafv  47412  fundcmpsurbijinj  47415  fundcmpsurinjALT  47417  fmtnoinf  47541  isubgruhgr  47872  upgrimwlklem1  47901  elbigolo1  48550