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  7282  nn0supp  9320  frecuzrdg0  10524  frecuzrdgsuc  10525  frecuzrdgdomlem  10528  frecuzrdg0t  10533  frecuzrdgsuctlem  10534  climdm  11479  sum0  11572  isumz  11573  fsumsersdc  11579  isumclim  11605  zprodap0  11765  psrbaglesuppg  14306  iscnp3  14547  cnpnei  14563  cnclima  14567  cnrest2  14580  hmeores  14659  metcnp  14856  qtopbasss  14865  tgqioo  14899  dvaddxx  15047  dvmulxx  15048  dviaddf  15049  dvimulf  15050  dvef  15071  pilem3  15127