Theorem ffun 6725

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

Syntax hints:   → wi 4  Fun wfun 6542   Fn wfn 6543  ⟶wf 6544

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 206  df-an 396  df-fn 6551  df-f 6552

This theorem is referenced by:  ffund  6726  fco  6747  funssxp  6752  f00  6779  f1cof1  6804  fimadmfoALT  6822  fimacnvOLD  7080  dff3  7110  fliftf  7323  fiun  7946  f1iun  7947  fsuppeq  8180  fsuppeqg  8181  pmfun  8866  pmresg  8889  fodomr  9153  ac6sfi  9312  fissuni  9382  fipreima  9383  ffsuppbi  9422  cnfcomlem  9723  tcrank  9908  fseqenlem2  10049  carduniima  10120  infmap2  10242  hsmexlem4  10453  hsmexlem5  10454  axdc3lem2  10475  axdc3lem4  10477  smobeth  10610  fpwwe2lem12  10666  inar1  10799  grur1  10844  nqerid  10957  fcdmnn0fsuppg  12562  zexALT  12609  hashkf  14324  hashgval  14325  revco  14818  ccatco  14819  pfxco  14822  lswco  14823  climdm  15531  isercolllem2  15645  isercolllem3  15646  isercoll  15647  sum0  15700  sumz  15701  fsumsers  15707  isumclim  15736  ntrivcvgfvn0  15878  ntrivcvgtail  15879  zprodn0  15916  iprodclim  15975  znnen  16189  isacs2  17633  isacs5  18540  dprdss  19986  dprd2dlem1  19998  dmdprdsplit2lem  20002  iscnp3  23161  subbascn  23171  cnpnei  23181  cnclima  23185  iscncl  23186  cncls  23191  cnrest2  23203  cnhaus  23271  kgencn3  23475  xkopt  23572  xkococnlem  23576  hmeores  23688  fbasrn  23801  uzrest  23814  rnelfmlem  23869  rnelfm  23870  fmfnfmlem3  23873  fmfnfmlem4  23874  fmfnfm  23875  cnflf2  23920  metcnp  24463  metustsym  24477  cfilucfil  24481  restmetu  24492  qtopbaslem  24688  tgqioo  24729  re2ndc  24730  bndth  24897  tcphcph  25178  ovolficcss  25411  volf  25471  volsup  25498  uniioombllem3a  25526  uniioombllem4  25528  uniioombllem5  25529  dyadmbllem  25541  dyadmbl  25542  opnmbllem  25543  opnmblALT  25545  mbfimaicc  25573  ismbf3d  25596  mbfimaopnlem  25597  mbfimaopn2  25599  i1fima  25620  i1fima2  25621  i1fd  25623  itg1addlem4  25641  itg1addlem4OLD  25642  dvidlem  25857  dvcnp  25861  dvadd  25884  dvmul  25885  dvaddf  25886  dvmulf  25887  dvco  25892  dvcof  25893  dvcjbr  25894  dvcj  25895  dvrec  25900  dvcnvlem  25921  dvef  25925  dvferm1  25930  dvferm2  25932  c1liplem1  25942  dvcnvrelem2  25964  mdegcl  26018  deg1n0ima  26038  plyco0  26139  plypf1  26159  tayl0  26309  ulmdvlem3  26351  pserdv  26379  dvlog  26598  efopn  26605  relogbf  26736  nofun  27595  madeval  27792  oldf  27797  oldlim  27826  subusgr  29115  pthdivtx  29556  pthdlem2lem  29594  issh2  31032  hlimuni  31061  hhsscms  31101  occllem  31126  occl  31127  chscllem4  31463  imaelshi  31881  xrofsup  32550  tocyc01  32852  dimval  33298  dimvalfi  33299  smatrcl  33397  mdetpmtr1  33424  locfinreflem  33441  fsumcvg4  33551  zrhunitpreima  33579  imambfm  33882  carsggect  33938  sibfof  33960  eulerpartlemt  33991  eulerpartlemmf  33995  eulerpartlemgvv  33996  eulerpartlemgf  33999  rpsqrtcn  34225  cardpred  34713  nummin  34714  erdszelem2  34802  erdszelem7  34807  erdszelem8  34808  cvmliftlem15  34908  mrsub0  35126  mrsubccat  35128  mrsubcn  35129  mthmblem  35190  ivthALT  35819  icoreunrn  36838  icoreelrn  36840  curf  37071  curunc  37075  heicant  37128  opnmbllem0  37129  mblfinlem1  37130  itg2addnclem  37144  itg2addnclem2  37145  ftc1anclem7  37172  ftc1anc  37174  ftc2nc  37175  indexdom  37207  cnres2  37236  aks6d1c6lem2  41643  elrfirn  42115  fnwe2lem2  42475  arearect  42643  areaquad  42644  naddcnff  42791  dfno2  42858  absfun  44732  evthiccabs  44881  ioofun  44936  cncficcgt0  45276  fperdvper  45307  fvvolioof  45377  fvvolicof  45379  fourierdlem20  45515  fourierdlem42  45537  fourierdlem63  45557  fourierdlem76  45570  fourierdlem93  45587  fourierdlem97  45591  fourierdlem113  45607  ovolval3  46035  uniimafveqt  46721  fundcmpsurbijinjpreimafv  46747  fundcmpsurbijinj  46750  fundcmpsurinjALT  46752  fmtnoinf  46876  elbigolo1  47630