Theorem ffun 5410

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

Syntax hints:   -> wi 4   Fun wfun 5252   Fn wfn 5253   -->wf 5254

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 5261  df-f 5262

This theorem is referenced by:  ffund  5411  funssxp  5427  f00  5449  fofun  5481  fun11iun  5525  fimacnv  5691  dff3im  5707  resflem  5726  fmptco  5728  fliftf  5846  smores2  6352  pmfun  6727  elmapfun  6731  pmresg  6735  ac6sfi  6959  casef  7154  omp1eomlem  7160  ctm  7175  exmidfodomrlemim  7268  nn0supp  9301  frecuzrdg0  10505  frecuzrdgsuc  10506  frecuzrdgdomlem  10509  frecuzrdg0t  10514  frecuzrdgsuctlem  10515  climdm  11460  sum0  11553  isumz  11554  fsumsersdc  11560  isumclim  11586  zprodap0  11746  psrbaglesuppg  14226  iscnp3  14439  cnpnei  14455  cnclima  14459  cnrest2  14472  hmeores  14551  metcnp  14748  qtopbasss  14757  tgqioo  14791  dvaddxx  14939  dvmulxx  14940  dviaddf  14941  dvimulf  14942  dvef  14963  pilem3  15019