Theorem ffun 5340

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 5337	. 2 |- ( F : A --> B -> F Fn A )
2		fnfun 5285	. 2 |- ( F Fn A -> Fun F )
3	1, 2	syl 14	1 |- ( F : A --> B -> Fun F )

Syntax hints:   -> wi 4   Fun wfun 5182   Fn wfn 5183   -->wf 5184

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

This theorem depends on definitions:  df-bi 116  df-fn 5191  df-f 5192

This theorem is referenced by:  ffund  5341  funssxp  5357  f00  5379  fofun  5411  fun11iun  5453  fimacnv  5614  dff3im  5630  resflem  5649  fmptco  5651  fliftf  5767  smores2  6262  pmfun  6634  elmapfun  6638  pmresg  6642  ac6sfi  6864  casef  7053  omp1eomlem  7059  ctm  7074  exmidfodomrlemim  7157  nn0supp  9166  frecuzrdg0  10348  frecuzrdgsuc  10349  frecuzrdgdomlem  10352  frecuzrdg0t  10357  frecuzrdgsuctlem  10358  climdm  11236  sum0  11329  isumz  11330  fsumsersdc  11336  isumclim  11362  zprodap0  11522  iscnp3  12843  cnpnei  12859  cnclima  12863  cnrest2  12876  hmeores  12955  metcnp  13152  qtopbasss  13161  tgqioo  13187  dvaddxx  13307  dvmulxx  13308  dviaddf  13309  dvimulf  13310  dvef  13328  pilem3  13344