Theorem ffun 6721

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

Syntax hints:   → wi 4  Fun wfun 6538   Fn wfn 6539  ⟶wf 6540

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 398  df-fn 6547  df-f 6548

This theorem is referenced by:  ffund  6722  fco  6742  funssxp  6747  f00  6774  f1cof1  6799  fimadmfoALT  6817  fimacnvOLD  7073  dff3  7102  fliftf  7312  fiun  7929  f1iun  7930  fsuppeq  8160  fsuppeqg  8161  pmfun  8841  pmresg  8864  fodomr  9128  ac6sfi  9287  fissuni  9357  fipreima  9358  ffsuppbi  9393  cnfcomlem  9694  tcrank  9879  fseqenlem2  10020  carduniima  10091  infmap2  10213  hsmexlem4  10424  hsmexlem5  10425  axdc3lem2  10446  axdc3lem4  10448  smobeth  10581  fpwwe2lem12  10637  inar1  10770  grur1  10815  nqerid  10928  fcdmnn0fsuppg  12531  zexALT  12578  hashkf  14292  hashgval  14293  revco  14785  ccatco  14786  pfxco  14789  lswco  14790  climdm  15498  isercolllem2  15612  isercolllem3  15613  isercoll  15614  sum0  15667  sumz  15668  fsumsers  15674  isumclim  15703  ntrivcvgfvn0  15845  ntrivcvgtail  15846  zprodn0  15883  iprodclim  15942  znnen  16155  isacs2  17597  isacs5  18501  dprdss  19899  dprd2dlem1  19911  dmdprdsplit2lem  19915  iscnp3  22748  subbascn  22758  cnpnei  22768  cnclima  22772  iscncl  22773  cncls  22778  cnrest2  22790  cnhaus  22858  kgencn3  23062  xkopt  23159  xkococnlem  23163  hmeores  23275  fbasrn  23388  uzrest  23401  rnelfmlem  23456  rnelfm  23457  fmfnfmlem3  23460  fmfnfmlem4  23461  fmfnfm  23462  cnflf2  23507  metcnp  24050  metustsym  24064  cfilucfil  24068  restmetu  24079  qtopbaslem  24275  tgqioo  24316  re2ndc  24317  bndth  24474  tcphcph  24754  ovolficcss  24986  volf  25046  volsup  25073  uniioombllem3a  25101  uniioombllem4  25103  uniioombllem5  25104  dyadmbllem  25116  dyadmbl  25117  opnmbllem  25118  opnmblALT  25120  mbfimaicc  25148  ismbf3d  25171  mbfimaopnlem  25172  mbfimaopn2  25174  i1fima  25195  i1fima2  25196  i1fd  25198  itg1addlem4  25216  itg1addlem4OLD  25217  dvidlem  25432  dvcnp  25436  dvadd  25457  dvmul  25458  dvaddf  25459  dvmulf  25460  dvco  25464  dvcof  25465  dvcjbr  25466  dvcj  25467  dvrec  25472  dvcnvlem  25493  dvef  25497  dvferm1  25502  dvferm2  25504  c1liplem1  25513  dvcnvrelem2  25535  mdegcl  25587  deg1n0ima  25607  plyco0  25706  plypf1  25726  tayl0  25874  ulmdvlem3  25914  pserdv  25941  dvlog  26159  efopn  26166  relogbf  26296  nofun  27152  madeval  27347  oldf  27352  oldlim  27381  subusgr  28546  pthdivtx  28986  pthdlem2lem  29024  issh2  30462  hlimuni  30491  hhsscms  30531  occllem  30556  occl  30557  chscllem4  30893  imaelshi  31311  xrofsup  31980  tocyc01  32277  dimval  32686  dimvalfi  32687  smatrcl  32776  mdetpmtr1  32803  locfinreflem  32820  fsumcvg4  32930  zrhunitpreima  32958  imambfm  33261  carsggect  33317  sibfof  33339  eulerpartlemt  33370  eulerpartlemmf  33374  eulerpartlemgvv  33375  eulerpartlemgf  33378  rpsqrtcn  33605  cardpred  34093  nummin  34094  erdszelem2  34183  erdszelem7  34188  erdszelem8  34189  cvmliftlem15  34289  mrsub0  34507  mrsubccat  34509  mrsubcn  34510  mthmblem  34571  ivthALT  35220  icoreunrn  36240  icoreelrn  36242  curf  36466  curunc  36470  heicant  36523  opnmbllem0  36524  mblfinlem1  36525  itg2addnclem  36539  itg2addnclem2  36540  ftc1anclem7  36567  ftc1anc  36569  ftc2nc  36570  indexdom  36602  cnres2  36631  elrfirn  41433  fnwe2lem2  41793  arearect  41964  areaquad  41965  naddcnff  42112  dfno2  42179  absfun  44060  evthiccabs  44209  ioofun  44264  cncficcgt0  44604  fperdvper  44635  fvvolioof  44705  fvvolicof  44707  fourierdlem20  44843  fourierdlem42  44865  fourierdlem63  44885  fourierdlem76  44898  fourierdlem93  44915  fourierdlem97  44919  fourierdlem113  44935  ovolval3  45363  uniimafveqt  46049  fundcmpsurbijinjpreimafv  46075  fundcmpsurbijinj  46078  fundcmpsurinjALT  46080  fmtnoinf  46204  elbigolo1  47243