Theorem ffun 5476

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

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

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

This theorem is referenced by:  ffund  5477  funssxp  5495  f00  5519  fofun  5551  fun11iun  5595  fimacnv  5766  dff3im  5782  resflem  5801  fmptco  5803  fliftf  5929  smores2  6446  pmfun  6823  elmapfun  6827  pmresg  6831  ac6sfi  7068  casef  7266  omp1eomlem  7272  ctm  7287  exmidfodomrlemim  7390  nn0supp  9432  frecuzrdg0  10647  frecuzrdgsuc  10648  frecuzrdgdomlem  10651  frecuzrdg0t  10656  frecuzrdgsuctlem  10657  climdm  11821  sum0  11914  isumz  11915  fsumsersdc  11921  isumclim  11947  zprodap0  12107  psrbaglesuppg  14651  iscnp3  14892  cnpnei  14908  cnclima  14912  cnrest2  14925  hmeores  15004  metcnp  15201  qtopbasss  15210  tgqioo  15244  dvaddxx  15392  dvmulxx  15393  dviaddf  15394  dvimulf  15395  dvef  15416  pilem3  15472  upgr2wlkdc  16116