Theorem ffun 5407

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

Syntax hints:   -> wi 4   Fun wfun 5249   Fn wfn 5250   -->wf 5251

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 5258  df-f 5259

This theorem is referenced by:  ffund  5408  funssxp  5424  f00  5446  fofun  5478  fun11iun  5522  fimacnv  5688  dff3im  5704  resflem  5723  fmptco  5725  fliftf  5843  smores2  6349  pmfun  6724  elmapfun  6728  pmresg  6732  ac6sfi  6956  casef  7149  omp1eomlem  7155  ctm  7170  exmidfodomrlemim  7263  nn0supp  9295  frecuzrdg0  10487  frecuzrdgsuc  10488  frecuzrdgdomlem  10491  frecuzrdg0t  10496  frecuzrdgsuctlem  10497  climdm  11441  sum0  11534  isumz  11535  fsumsersdc  11541  isumclim  11567  zprodap0  11727  psrbaglesuppg  14169  iscnp3  14382  cnpnei  14398  cnclima  14402  cnrest2  14415  hmeores  14494  metcnp  14691  qtopbasss  14700  tgqioo  14734  dvaddxx  14882  dvmulxx  14883  dviaddf  14884  dvimulf  14885  dvef  14906  pilem3  14959