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  5493  f00  5517  fofun  5549  fun11iun  5593  fimacnv  5764  dff3im  5780  resflem  5799  fmptco  5801  fliftf  5923  smores2  6440  pmfun  6815  elmapfun  6819  pmresg  6823  ac6sfi  7060  casef  7255  omp1eomlem  7261  ctm  7276  exmidfodomrlemim  7379  nn0supp  9421  frecuzrdg0  10635  frecuzrdgsuc  10636  frecuzrdgdomlem  10639  frecuzrdg0t  10644  frecuzrdgsuctlem  10645  climdm  11806  sum0  11899  isumz  11900  fsumsersdc  11906  isumclim  11932  zprodap0  12092  psrbaglesuppg  14636  iscnp3  14877  cnpnei  14893  cnclima  14897  cnrest2  14910  hmeores  14989  metcnp  15186  qtopbasss  15195  tgqioo  15229  dvaddxx  15377  dvmulxx  15378  dviaddf  15379  dvimulf  15380  dvef  15401  pilem3  15457