Theorem ffun 5164

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

Syntax hints:   -> wi 4   Fun wfun 5009   Fn wfn 5010   -->wf 5011

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

This theorem depends on definitions:  df-bi 115  df-fn 5018  df-f 5019

This theorem is referenced by:  funssxp  5180  f00  5202  fofun  5234  fun11iun  5274  fimacnv  5428  dff3im  5444  resflem  5462  fmptco  5464  fliftf  5578  smores2  6059  pmfun  6423  elmapfun  6427  pmresg  6431  ac6sfi  6612  casef  6777  exmidfodomrlemim  6825  nn0supp  8723  frecuzrdg0  9816  frecuzrdgsuc  9817  frecuzrdgdomlem  9820  frecuzrdg0t  9825  frecuzrdgsuctlem  9826  climdm  10679  sum0  10776  isumz  10777  fisumsers  10784  isumclim  10811