Theorem ffun 5443

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

Syntax hints:   -> wi 4   Fun wfun 5279   Fn wfn 5280   -->wf 5281

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 5288  df-f 5289

This theorem is referenced by:  ffund  5444  funssxp  5460  f00  5484  fofun  5516  fun11iun  5560  fimacnv  5727  dff3im  5743  resflem  5762  fmptco  5764  fliftf  5886  smores2  6398  pmfun  6773  elmapfun  6777  pmresg  6781  ac6sfi  7016  casef  7211  omp1eomlem  7217  ctm  7232  exmidfodomrlemim  7335  nn0supp  9377  frecuzrdg0  10590  frecuzrdgsuc  10591  frecuzrdgdomlem  10594  frecuzrdg0t  10599  frecuzrdgsuctlem  10600  climdm  11691  sum0  11784  isumz  11785  fsumsersdc  11791  isumclim  11817  zprodap0  11977  psrbaglesuppg  14519  iscnp3  14760  cnpnei  14776  cnclima  14780  cnrest2  14793  hmeores  14872  metcnp  15069  qtopbasss  15078  tgqioo  15112  dvaddxx  15260  dvmulxx  15261  dviaddf  15262  dvimulf  15263  dvef  15284  pilem3  15340