Theorem ffun 5475

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

Syntax hints:   -> wi 4   Fun wfun 5311   Fn wfn 5312   -->wf 5313

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 5320  df-f 5321

This theorem is referenced by:  ffund  5476  funssxp  5492  f00  5516  fofun  5548  fun11iun  5592  fimacnv  5763  dff3im  5779  resflem  5798  fmptco  5800  fliftf  5922  smores2  6438  pmfun  6813  elmapfun  6817  pmresg  6821  ac6sfi  7056  casef  7251  omp1eomlem  7257  ctm  7272  exmidfodomrlemim  7375  nn0supp  9417  frecuzrdg0  10630  frecuzrdgsuc  10631  frecuzrdgdomlem  10634  frecuzrdg0t  10639  frecuzrdgsuctlem  10640  climdm  11801  sum0  11894  isumz  11895  fsumsersdc  11901  isumclim  11927  zprodap0  12087  psrbaglesuppg  14630  iscnp3  14871  cnpnei  14887  cnclima  14891  cnrest2  14904  hmeores  14983  metcnp  15180  qtopbasss  15189  tgqioo  15223  dvaddxx  15371  dvmulxx  15372  dviaddf  15373  dvimulf  15374  dvef  15395  pilem3  15451