Theorem ffun 6707

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

Syntax hints:   → wi 4  Fun wfun 6526   Fn wfn 6527  ⟶wf 6528

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 397  df-fn 6535  df-f 6536

This theorem is referenced by:  ffund  6708  fco  6728  funssxp  6733  f00  6760  f1cof1  6785  fimadmfoALT  6803  fimacnvOLD  7057  dff3  7086  fliftf  7296  fiun  7911  f1iun  7912  fsuppeq  8142  fsuppeqg  8143  pmfun  8824  pmresg  8847  fodomr  9111  ac6sfi  9270  fissuni  9340  fipreima  9341  ffsuppbi  9375  cnfcomlem  9676  tcrank  9861  fseqenlem2  10002  carduniima  10073  infmap2  10195  hsmexlem4  10406  hsmexlem5  10407  axdc3lem2  10428  axdc3lem4  10430  smobeth  10563  fpwwe2lem12  10619  inar1  10752  grur1  10797  nqerid  10910  fcdmnn0fsuppg  12513  zexALT  12560  hashkf  14274  hashgval  14275  revco  14767  ccatco  14768  pfxco  14771  lswco  14772  climdm  15480  isercolllem2  15594  isercolllem3  15595  isercoll  15596  sum0  15649  sumz  15650  fsumsers  15656  isumclim  15685  ntrivcvgfvn0  15827  ntrivcvgtail  15828  zprodn0  15865  iprodclim  15924  znnen  16137  isacs2  17579  isacs5  18483  dprdss  19858  dprd2dlem1  19870  dmdprdsplit2lem  19874  iscnp3  22677  subbascn  22687  cnpnei  22697  cnclima  22701  iscncl  22702  cncls  22707  cnrest2  22719  cnhaus  22787  kgencn3  22991  xkopt  23088  xkococnlem  23092  hmeores  23204  fbasrn  23317  uzrest  23330  rnelfmlem  23385  rnelfm  23386  fmfnfmlem3  23389  fmfnfmlem4  23390  fmfnfm  23391  cnflf2  23436  metcnp  23979  metustsym  23993  cfilucfil  23997  restmetu  24008  qtopbaslem  24204  tgqioo  24245  re2ndc  24246  bndth  24403  tcphcph  24683  ovolficcss  24915  volf  24975  volsup  25002  uniioombllem3a  25030  uniioombllem4  25032  uniioombllem5  25033  dyadmbllem  25045  dyadmbl  25046  opnmbllem  25047  opnmblALT  25049  mbfimaicc  25077  ismbf3d  25100  mbfimaopnlem  25101  mbfimaopn2  25103  i1fima  25124  i1fima2  25125  i1fd  25127  itg1addlem4  25145  itg1addlem4OLD  25146  dvidlem  25361  dvcnp  25365  dvadd  25386  dvmul  25387  dvaddf  25388  dvmulf  25389  dvco  25393  dvcof  25394  dvcjbr  25395  dvcj  25396  dvrec  25401  dvcnvlem  25422  dvef  25426  dvferm1  25431  dvferm2  25433  c1liplem1  25442  dvcnvrelem2  25464  mdegcl  25516  deg1n0ima  25536  plyco0  25635  plypf1  25655  tayl0  25803  ulmdvlem3  25843  pserdv  25870  dvlog  26088  efopn  26095  relogbf  26223  nofun  27079  madeval  27270  oldf  27275  oldlim  27304  subusgr  28411  pthdivtx  28851  pthdlem2lem  28889  issh2  30325  hlimuni  30354  hhsscms  30394  occllem  30419  occl  30420  chscllem4  30756  imaelshi  31174  xrofsup  31851  tocyc01  32148  dimval  32525  dimvalfi  32526  smatrcl  32607  mdetpmtr1  32634  locfinreflem  32651  fsumcvg4  32761  zrhunitpreima  32789  imambfm  33092  carsggect  33148  sibfof  33170  eulerpartlemt  33201  eulerpartlemmf  33205  eulerpartlemgvv  33206  eulerpartlemgf  33209  rpsqrtcn  33436  cardpred  33924  nummin  33925  erdszelem2  34014  erdszelem7  34019  erdszelem8  34020  cvmliftlem15  34120  mrsub0  34338  mrsubccat  34340  mrsubcn  34341  mthmblem  34402  ivthALT  35024  icoreunrn  36044  icoreelrn  36046  curf  36270  curunc  36274  heicant  36327  opnmbllem0  36328  mblfinlem1  36329  itg2addnclem  36343  itg2addnclem2  36344  ftc1anclem7  36371  ftc1anc  36373  ftc2nc  36374  indexdom  36407  cnres2  36436  elrfirn  41204  fnwe2lem2  41564  arearect  41735  areaquad  41736  naddcnff  41883  dfno2  41950  absfun  43833  evthiccabs  43982  ioofun  44037  cncficcgt0  44377  fperdvper  44408  fvvolioof  44478  fvvolicof  44480  fourierdlem20  44616  fourierdlem42  44638  fourierdlem63  44658  fourierdlem76  44671  fourierdlem93  44688  fourierdlem97  44692  fourierdlem113  44708  ovolval3  45136  uniimafveqt  45821  fundcmpsurbijinjpreimafv  45847  fundcmpsurbijinj  45850  fundcmpsurinjALT  45852  fmtnoinf  45976  elbigolo1  46891