Theorem ffun 6750

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

Syntax hints:   → wi 4  Fun wfun 6567   Fn wfn 6568  ⟶wf 6569

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 6576  df-f 6577

This theorem is referenced by:  ffund  6751  fco  6771  funssxp  6776  f00  6803  f1cof1  6827  fimadmfoALT  6845  fimacnvOLD  7104  dff3  7134  fliftf  7351  fiun  7983  f1iun  7984  fsuppeq  8216  fsuppeqg  8217  pmfun  8905  pmresg  8928  fodomr  9194  ac6sfi  9348  fodomfir  9396  fissuni  9427  fipreima  9428  ffsuppbi  9467  cnfcomlem  9768  tcrank  9953  fseqenlem2  10094  carduniima  10165  infmap2  10286  hsmexlem4  10498  hsmexlem5  10499  axdc3lem2  10520  axdc3lem4  10522  smobeth  10655  fpwwe2lem12  10711  inar1  10844  grur1  10889  nqerid  11002  fcdmnn0fsuppg  12612  zexALT  12659  hashkf  14381  hashgval  14382  revco  14883  ccatco  14884  pfxco  14887  lswco  14888  climdm  15600  isercolllem2  15714  isercolllem3  15715  isercoll  15716  sum0  15769  sumz  15770  fsumsers  15776  isumclim  15805  ntrivcvgfvn0  15947  ntrivcvgtail  15948  zprodn0  15987  iprodclim  16046  znnen  16260  isacs2  17711  isacs5  18618  dprdss  20073  dprd2dlem1  20085  dmdprdsplit2lem  20089  iscnp3  23273  subbascn  23283  cnpnei  23293  cnclima  23297  iscncl  23298  cncls  23303  cnrest2  23315  cnhaus  23383  kgencn3  23587  xkopt  23684  xkococnlem  23688  hmeores  23800  fbasrn  23913  uzrest  23926  rnelfmlem  23981  rnelfm  23982  fmfnfmlem3  23985  fmfnfmlem4  23986  fmfnfm  23987  cnflf2  24032  metcnp  24575  metustsym  24589  cfilucfil  24593  restmetu  24604  qtopbaslem  24800  tgqioo  24841  re2ndc  24842  bndth  25009  tcphcph  25290  ovolficcss  25523  volf  25583  volsup  25610  uniioombllem3a  25638  uniioombllem4  25640  uniioombllem5  25641  dyadmbllem  25653  dyadmbl  25654  opnmbllem  25655  opnmblALT  25657  mbfimaicc  25685  ismbf3d  25708  mbfimaopnlem  25709  mbfimaopn2  25711  i1fima  25732  i1fima2  25733  i1fd  25735  itg1addlem4  25753  itg1addlem4OLD  25754  dvidlem  25970  dvcnp  25974  dvadd  25997  dvmul  25998  dvaddf  25999  dvmulf  26000  dvco  26005  dvcof  26006  dvcjbr  26007  dvcj  26008  dvrec  26013  dvcnvlem  26034  dvef  26038  dvferm1  26043  dvferm2  26045  c1liplem1  26055  dvcnvrelem2  26077  mdegcl  26128  deg1n0ima  26148  plyco0  26251  plypf1  26271  tayl0  26421  ulmdvlem3  26463  pserdv  26491  dvlog  26711  efopn  26718  relogbf  26852  nofun  27712  madeval  27909  oldf  27914  oldlim  27943  madefi  27968  oldfi  27969  subusgr  29324  pthdivtx  29765  pthdlem2lem  29803  issh2  31241  hlimuni  31270  hhsscms  31310  occllem  31335  occl  31336  chscllem4  31672  imaelshi  32090  xrofsup  32774  tocyc01  33111  dimval  33613  dimvalfi  33614  smatrcl  33742  mdetpmtr1  33769  locfinreflem  33786  fsumcvg4  33896  zrhunitpreima  33924  imambfm  34227  carsggect  34283  sibfof  34305  eulerpartlemt  34336  eulerpartlemmf  34340  eulerpartlemgvv  34341  eulerpartlemgf  34344  rpsqrtcn  34570  cardpred  35066  nummin  35067  erdszelem2  35160  erdszelem7  35165  erdszelem8  35166  cvmliftlem15  35266  mrsub0  35484  mrsubccat  35486  mrsubcn  35487  mthmblem  35548  ivthALT  36301  icoreunrn  37325  icoreelrn  37327  curf  37558  curunc  37562  heicant  37615  opnmbllem0  37616  mblfinlem1  37617  itg2addnclem  37631  itg2addnclem2  37632  ftc1anclem7  37659  ftc1anc  37661  ftc2nc  37662  indexdom  37694  cnres2  37723  aks6d1c6lem2  42128  elrfirn  42651  fnwe2lem2  43008  arearect  43176  areaquad  43177  naddcnff  43324  dfno2  43390  absfun  45265  evthiccabs  45414  ioofun  45469  cncficcgt0  45809  fperdvper  45840  fvvolioof  45910  fvvolicof  45912  fourierdlem20  46048  fourierdlem42  46070  fourierdlem63  46090  fourierdlem76  46103  fourierdlem93  46120  fourierdlem97  46124  fourierdlem113  46140  ovolval3  46568  uniimafveqt  47255  fundcmpsurbijinjpreimafv  47281  fundcmpsurbijinj  47284  fundcmpsurinjALT  47286  fmtnoinf  47410  isubgruhgr  47738  elbigolo1  48291