Theorem ffun 5413

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

Syntax hints:   -> wi 4   Fun wfun 5253   Fn wfn 5254   -->wf 5255

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 5262  df-f 5263

This theorem is referenced by:  ffund  5414  funssxp  5430  f00  5452  fofun  5484  fun11iun  5528  fimacnv  5694  dff3im  5710  resflem  5729  fmptco  5731  fliftf  5849  smores2  6361  pmfun  6736  elmapfun  6740  pmresg  6744  ac6sfi  6968  casef  7163  omp1eomlem  7169  ctm  7184  exmidfodomrlemim  7280  nn0supp  9318  frecuzrdg0  10522  frecuzrdgsuc  10523  frecuzrdgdomlem  10526  frecuzrdg0t  10531  frecuzrdgsuctlem  10532  climdm  11477  sum0  11570  isumz  11571  fsumsersdc  11577  isumclim  11603  zprodap0  11763  psrbaglesuppg  14302  iscnp3  14523  cnpnei  14539  cnclima  14543  cnrest2  14556  hmeores  14635  metcnp  14832  qtopbasss  14841  tgqioo  14875  dvaddxx  15023  dvmulxx  15024  dviaddf  15025  dvimulf  15026  dvef  15047  pilem3  15103