Theorem ffun 5482

Description: A mapping is a function. (Contributed by NM, 3-Aug-1994.)

Assertion

Ref	Expression
ffun	|- ( F : A --> B -> Fun F )

Proof of Theorem ffun

Step	Hyp	Ref	Expression
1		ffn 5479	. 2 |- ( F : A --> B -> F Fn A )
2		fnfun 5424	. 2 |- ( F Fn A -> Fun F )
3	1, 2	syl 14	1 |- ( F : A --> B -> Fun F )

Syntax hints:   -> wi 4   Fun wfun 5318   Fn wfn 5319   -->wf 5320

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-fn 5327  df-f 5328

This theorem is referenced by:  ffund  5483  funssxp  5501  f00  5525  fofun  5557  fun11iun  5601  fimacnv  5772  dff3im  5788  resflem  5807  fmptco  5809  fliftf  5935  smores2  6455  pmfun  6832  elmapfun  6836  pmresg  6840  ac6sfi  7080  casef  7278  omp1eomlem  7284  ctm  7299  exmidfodomrlemim  7402  nn0supp  9444  frecuzrdg0  10665  frecuzrdgsuc  10666  frecuzrdgdomlem  10669  frecuzrdg0t  10674  frecuzrdgsuctlem  10675  climdm  11846  sum0  11939  isumz  11940  fsumsersdc  11946  isumclim  11972  zprodap0  12132  psrbaglesuppg  14676  iscnp3  14917  cnpnei  14933  cnclima  14937  cnrest2  14950  hmeores  15029  metcnp  15226  qtopbasss  15235  tgqioo  15269  dvaddxx  15417  dvmulxx  15418  dviaddf  15419  dvimulf  15420  dvef  15441  pilem3  15497  upgr2wlkdc  16172