Theorem ffun 6654

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

Syntax hints:   → wi 4  Fun wfun 6475   Fn wfn 6476  ⟶wf 6477

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 6484  df-f 6485

This theorem is referenced by:  ffund  6655  fco  6675  funssxp  6679  f00  6705  f1cof1  6729  fimadmfoALT  6746  dff3  7033  fliftf  7249  fiun  7875  f1iun  7876  fsuppeq  8105  fsuppeqg  8106  pmfun  8771  pmresg  8794  fodomr  9041  ac6sfi  9168  fodomfir  9212  fissuni  9241  fipreima  9242  ffsuppbi  9282  cnfcomlem  9589  tcrank  9774  fseqenlem2  9913  carduniima  9984  infmap2  10105  hsmexlem4  10317  hsmexlem5  10318  axdc3lem2  10339  axdc3lem4  10341  smobeth  10474  fpwwe2lem12  10530  inar1  10663  grur1  10708  nqerid  10821  fcdmnn0fsuppg  12438  zexALT  12485  hashkf  14236  hashgval  14237  revco  14738  ccatco  14739  pfxco  14742  lswco  14743  climdm  15458  isercolllem2  15570  isercolllem3  15571  isercoll  15572  sum0  15625  sumz  15626  fsumsers  15632  isumclim  15661  ntrivcvgfvn0  15803  ntrivcvgtail  15804  zprodn0  15843  iprodclim  15902  znnen  16118  isacs2  17556  isacs5  18451  dprdss  19941  dprd2dlem1  19953  dmdprdsplit2lem  19957  iscnp3  23157  subbascn  23167  cnpnei  23177  cnclima  23181  iscncl  23182  cncls  23187  cnrest2  23199  cnhaus  23267  kgencn3  23471  xkopt  23568  xkococnlem  23572  hmeores  23684  fbasrn  23797  uzrest  23810  rnelfmlem  23865  rnelfm  23866  fmfnfmlem3  23869  fmfnfmlem4  23870  fmfnfm  23871  cnflf2  23916  metcnp  24454  metustsym  24468  cfilucfil  24472  restmetu  24483  qtopbaslem  24671  tgqioo  24713  re2ndc  24714  bndth  24882  tcphcph  25162  ovolficcss  25395  volf  25455  volsup  25482  uniioombllem3a  25510  uniioombllem4  25512  uniioombllem5  25513  dyadmbllem  25525  dyadmbl  25526  opnmbllem  25527  opnmblALT  25529  mbfimaicc  25557  ismbf3d  25580  mbfimaopnlem  25581  mbfimaopn2  25583  i1fima  25604  i1fima2  25605  i1fd  25607  itg1addlem4  25625  dvidlem  25841  dvcnp  25845  dvadd  25868  dvmul  25869  dvaddf  25870  dvmulf  25871  dvco  25876  dvcof  25877  dvcjbr  25878  dvcj  25879  dvrec  25884  dvcnvlem  25905  dvef  25909  dvferm1  25914  dvferm2  25916  c1liplem1  25926  dvcnvrelem2  25948  mdegcl  25999  deg1n0ima  26019  plyco0  26122  plypf1  26142  tayl0  26294  ulmdvlem3  26336  pserdv  26364  dvlog  26585  efopn  26592  relogbf  26726  nofun  27586  madeval  27791  oldf  27796  oldlim  27830  madefi  27856  oldfi  27857  subusgr  29265  pthdivtx  29703  pthdlem2lem  29743  cyclnumvtx  29776  issh2  31184  hlimuni  31213  hhsscms  31253  occllem  31278  occl  31279  chscllem4  31615  imaelshi  32033  xrofsup  32745  tocyc01  33082  exsslsb  33604  dimval  33608  dimvalfi  33609  smatrcl  33804  mdetpmtr1  33831  locfinreflem  33848  fsumcvg4  33958  zrhunitpreima  33984  imambfm  34270  carsggect  34326  sibfof  34348  eulerpartlemt  34379  eulerpartlemmf  34383  eulerpartlemgvv  34384  eulerpartlemgf  34387  rpsqrtcn  34601  cardpred  35098  nummin  35099  erdszelem2  35224  erdszelem7  35229  erdszelem8  35230  cvmliftlem15  35330  mrsub0  35548  mrsubccat  35550  mrsubcn  35551  mthmblem  35612  ivthALT  36368  icoreunrn  37392  icoreelrn  37394  curf  37637  curunc  37641  heicant  37694  opnmbllem0  37695  mblfinlem1  37696  itg2addnclem  37710  itg2addnclem2  37711  ftc1anclem7  37738  ftc1anc  37740  ftc2nc  37741  indexdom  37773  cnres2  37802  aks6d1c6lem2  42203  elrfirn  42727  fnwe2lem2  43083  arearect  43247  areaquad  43248  naddcnff  43394  dfno2  43460  relpfr  44986  absfun  45388  evthiccabs  45535  ioofun  45590  cncficcgt0  45925  fperdvper  45956  fvvolioof  46026  fvvolicof  46028  fourierdlem20  46164  fourierdlem42  46186  fourierdlem63  46206  fourierdlem76  46219  fourierdlem93  46236  fourierdlem97  46240  fourierdlem113  46256  ovolval3  46684  tannpoly  46920  sinnpoly  46921  uniimafveqt  47411  fundcmpsurbijinjpreimafv  47437  fundcmpsurbijinj  47440  fundcmpsurinjALT  47442  fmtnoinf  47566  isubgruhgr  47898  upgrimwlklem1  47927  elbigolo1  48588