Theorem ffun 5387

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

Syntax hints:   -> wi 4   Fun wfun 5229   Fn wfn 5230   -->wf 5231

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 5238  df-f 5239

This theorem is referenced by:  ffund  5388  funssxp  5404  f00  5426  fofun  5458  fun11iun  5501  fimacnv  5666  dff3im  5682  resflem  5701  fmptco  5703  fliftf  5821  smores2  6319  pmfun  6694  elmapfun  6698  pmresg  6702  ac6sfi  6926  casef  7117  omp1eomlem  7123  ctm  7138  exmidfodomrlemim  7230  nn0supp  9258  frecuzrdg0  10444  frecuzrdgsuc  10445  frecuzrdgdomlem  10448  frecuzrdg0t  10453  frecuzrdgsuctlem  10454  climdm  11335  sum0  11428  isumz  11429  fsumsersdc  11435  isumclim  11461  zprodap0  11621  psrbaglesuppg  13950  iscnp3  14163  cnpnei  14179  cnclima  14183  cnrest2  14196  hmeores  14275  metcnp  14472  qtopbasss  14481  tgqioo  14507  dvaddxx  14627  dvmulxx  14628  dviaddf  14629  dvimulf  14630  dvef  14648  pilem3  14664