Theorem ffun 6499

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

Syntax hints:   → wi 4  Fun wfun 6327   Fn wfn 6328  ⟶wf 6329

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 210  df-an 401  df-fn 6336  df-f 6337

This theorem is referenced by:  ffund  6500  funssxp  6518  f00  6544  fimadmfoALT  6585  fimacnv  6828  dff3  6855  fliftf  7060  fiun  7646  f1iun  7647  frnsuppeq  7847  frnsuppeqg  7848  pmfun  8434  pmresg  8450  fodomr  8687  ac6sfi  8785  fissuni  8852  fipreima  8853  frnfsuppbi  8885  cnfcomlem  9185  tcrank  9336  fseqenlem2  9475  carduniima  9546  infmap2  9668  hsmexlem4  9879  hsmexlem5  9880  axdc3lem2  9901  axdc3lem4  9903  smobeth  10036  fpwwe2lem12  10092  inar1  10225  grur1  10270  nqerid  10383  frnnn0fsuppg  11983  zexALT  12030  hashkf  13732  hashgval  13733  revco  14233  ccatco  14234  pfxco  14237  lswco  14238  climdm  14949  isercolllem2  15060  isercolllem3  15061  isercoll  15062  sum0  15116  sumz  15117  fsumsers  15123  isumclim  15150  ntrivcvgfvn0  15293  ntrivcvgtail  15294  zprodn0  15331  iprodclim  15390  znnen  15603  isacs2  16972  isacs5  17838  dprdss  19209  dprd2dlem1  19221  dmdprdsplit2lem  19225  iscnp3  21934  subbascn  21944  cnpnei  21954  cnclima  21958  iscncl  21959  cncls  21964  cnrest2  21976  cnhaus  22044  kgencn3  22248  xkopt  22345  xkococnlem  22349  hmeores  22461  fbasrn  22574  uzrest  22587  rnelfmlem  22642  rnelfm  22643  fmfnfmlem3  22646  fmfnfmlem4  22647  fmfnfm  22648  cnflf2  22693  metcnp  23233  metustsym  23247  cfilucfil  23251  restmetu  23262  qtopbaslem  23450  tgqioo  23491  re2ndc  23492  bndth  23649  tcphcph  23927  ovolficcss  24159  volf  24219  volsup  24246  uniioombllem3a  24274  uniioombllem4  24276  uniioombllem5  24277  dyadmbllem  24289  dyadmbl  24290  opnmbllem  24291  opnmblALT  24293  mbfimaicc  24321  ismbf3d  24344  mbfimaopnlem  24345  mbfimaopn2  24347  i1fima  24368  i1fima2  24369  i1fd  24371  itg1addlem4  24389  dvidlem  24604  dvcnp  24608  dvadd  24629  dvmul  24630  dvaddf  24631  dvmulf  24632  dvco  24636  dvcof  24637  dvcjbr  24638  dvcj  24639  dvrec  24644  dvcnvlem  24665  dvef  24669  dvferm1  24674  dvferm2  24676  c1liplem1  24685  dvcnvrelem2  24707  mdegcl  24759  deg1n0ima  24779  plyco0  24878  plypf1  24898  tayl0  25046  ulmdvlem3  25086  pserdv  25113  dvlog  25331  efopn  25338  relogbf  25466  subusgr  27168  pthdivtx  27607  pthdlem2lem  27645  issh2  29081  hlimuni  29110  hhsscms  29150  occllem  29175  occl  29176  chscllem4  29512  imaelshi  29930  xrofsup  30604  tocyc01  30901  dimval  31197  dimvalfi  31198  smatrcl  31257  mdetpmtr1  31284  locfinreflem  31301  fsumcvg4  31411  zrhunitpreima  31437  imambfm  31738  carsggect  31794  sibfof  31816  eulerpartlemt  31847  eulerpartlemmf  31851  eulerpartlemgvv  31852  eulerpartlemgf  31855  rpsqrtcn  32082  cardpred  32581  nummin  32582  erdszelem2  32660  erdszelem7  32665  erdszelem8  32666  cvmliftlem15  32766  mrsub0  32984  mrsubccat  32986  mrsubcn  32987  mthmblem  33048  nofun  33407  madeval  33586  oldf  33591  oldlim  33616  ivthALT  34063  icoreunrn  35046  icoreelrn  35048  curf  35305  curunc  35309  heicant  35362  opnmbllem0  35363  mblfinlem1  35364  itg2addnclem  35378  itg2addnclem2  35379  ftc1anclem7  35406  ftc1anc  35408  ftc2nc  35409  indexdom  35442  cnres2  35471  elrfirn  39999  fnwe2lem2  40358  arearect  40528  areaquad  40529  absfun  42340  evthiccabs  42489  ioofun  42544  cncficcgt0  42886  fperdvper  42917  fvvolioof  42987  fvvolicof  42989  fourierdlem20  43125  fourierdlem42  43147  fourierdlem63  43167  fourierdlem76  43180  fourierdlem93  43197  fourierdlem97  43201  fourierdlem113  43217  ovolval3  43642  uniimafveqt  44256  fundcmpsurbijinjpreimafv  44282  fundcmpsurbijinj  44285  fundcmpsurinjALT  44287  fmtnoinf  44411  elbigolo1  45326