Theorem ffun 6739

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

Syntax hints:   → wi 4  Fun wfun 6556   Fn wfn 6557  ⟶wf 6558

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 6565  df-f 6566

This theorem is referenced by:  ffund  6740  fco  6760  funssxp  6764  f00  6790  f1cof1  6814  fimadmfoALT  6831  dff3  7119  fliftf  7334  fiun  7965  f1iun  7966  fsuppeq  8198  fsuppeqg  8199  pmfun  8885  pmresg  8908  fodomr  9166  ac6sfi  9317  fodomfir  9365  fissuni  9394  fipreima  9395  ffsuppbi  9435  cnfcomlem  9736  tcrank  9921  fseqenlem2  10062  carduniima  10133  infmap2  10254  hsmexlem4  10466  hsmexlem5  10467  axdc3lem2  10488  axdc3lem4  10490  smobeth  10623  fpwwe2lem12  10679  inar1  10812  grur1  10857  nqerid  10970  fcdmnn0fsuppg  12583  zexALT  12630  hashkf  14367  hashgval  14368  revco  14869  ccatco  14870  pfxco  14873  lswco  14874  climdm  15586  isercolllem2  15698  isercolllem3  15699  isercoll  15700  sum0  15753  sumz  15754  fsumsers  15760  isumclim  15789  ntrivcvgfvn0  15931  ntrivcvgtail  15932  zprodn0  15971  iprodclim  16030  znnen  16244  isacs2  17697  isacs5  18605  dprdss  20063  dprd2dlem1  20075  dmdprdsplit2lem  20079  iscnp3  23267  subbascn  23277  cnpnei  23287  cnclima  23291  iscncl  23292  cncls  23297  cnrest2  23309  cnhaus  23377  kgencn3  23581  xkopt  23678  xkococnlem  23682  hmeores  23794  fbasrn  23907  uzrest  23920  rnelfmlem  23975  rnelfm  23976  fmfnfmlem3  23979  fmfnfmlem4  23980  fmfnfm  23981  cnflf2  24026  metcnp  24569  metustsym  24583  cfilucfil  24587  restmetu  24598  qtopbaslem  24794  tgqioo  24835  re2ndc  24836  bndth  25003  tcphcph  25284  ovolficcss  25517  volf  25577  volsup  25604  uniioombllem3a  25632  uniioombllem4  25634  uniioombllem5  25635  dyadmbllem  25647  dyadmbl  25648  opnmbllem  25649  opnmblALT  25651  mbfimaicc  25679  ismbf3d  25702  mbfimaopnlem  25703  mbfimaopn2  25705  i1fima  25726  i1fima2  25727  i1fd  25729  itg1addlem4  25747  itg1addlem4OLD  25748  dvidlem  25964  dvcnp  25968  dvadd  25991  dvmul  25992  dvaddf  25993  dvmulf  25994  dvco  25999  dvcof  26000  dvcjbr  26001  dvcj  26002  dvrec  26007  dvcnvlem  26028  dvef  26032  dvferm1  26037  dvferm2  26039  c1liplem1  26049  dvcnvrelem2  26071  mdegcl  26122  deg1n0ima  26142  plyco0  26245  plypf1  26265  tayl0  26417  ulmdvlem3  26459  pserdv  26487  dvlog  26707  efopn  26714  relogbf  26848  nofun  27708  madeval  27905  oldf  27910  oldlim  27939  madefi  27964  oldfi  27965  subusgr  29320  pthdivtx  29761  pthdlem2lem  29799  issh2  31237  hlimuni  31266  hhsscms  31306  occllem  31331  occl  31332  chscllem4  31668  imaelshi  32086  xrofsup  32777  tocyc01  33120  dimval  33627  dimvalfi  33628  smatrcl  33756  mdetpmtr1  33783  locfinreflem  33800  fsumcvg4  33910  zrhunitpreima  33938  imambfm  34243  carsggect  34299  sibfof  34321  eulerpartlemt  34352  eulerpartlemmf  34356  eulerpartlemgvv  34357  eulerpartlemgf  34360  rpsqrtcn  34586  cardpred  35082  nummin  35083  erdszelem2  35176  erdszelem7  35181  erdszelem8  35182  cvmliftlem15  35282  mrsub0  35500  mrsubccat  35502  mrsubcn  35503  mthmblem  35564  ivthALT  36317  icoreunrn  37341  icoreelrn  37343  curf  37584  curunc  37588  heicant  37641  opnmbllem0  37642  mblfinlem1  37643  itg2addnclem  37657  itg2addnclem2  37658  ftc1anclem7  37685  ftc1anc  37687  ftc2nc  37688  indexdom  37720  cnres2  37749  aks6d1c6lem2  42152  elrfirn  42682  fnwe2lem2  43039  arearect  43203  areaquad  43204  naddcnff  43351  dfno2  43417  absfun  45299  evthiccabs  45448  ioofun  45503  cncficcgt0  45843  fperdvper  45874  fvvolioof  45944  fvvolicof  45946  fourierdlem20  46082  fourierdlem42  46104  fourierdlem63  46124  fourierdlem76  46137  fourierdlem93  46154  fourierdlem97  46158  fourierdlem113  46174  ovolval3  46602  uniimafveqt  47305  fundcmpsurbijinjpreimafv  47331  fundcmpsurbijinj  47334  fundcmpsurinjALT  47336  fmtnoinf  47460  isubgruhgr  47791  elbigolo1  48406