Theorem ffun 5427

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

Syntax hints:   -> wi 4   Fun wfun 5264   Fn wfn 5265   -->wf 5266

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 5273  df-f 5274

This theorem is referenced by:  ffund  5428  funssxp  5444  f00  5466  fofun  5498  fun11iun  5542  fimacnv  5708  dff3im  5724  resflem  5743  fmptco  5745  fliftf  5867  smores2  6379  pmfun  6754  elmapfun  6758  pmresg  6762  ac6sfi  6994  casef  7189  omp1eomlem  7195  ctm  7210  exmidfodomrlemim  7308  nn0supp  9346  frecuzrdg0  10556  frecuzrdgsuc  10557  frecuzrdgdomlem  10560  frecuzrdg0t  10565  frecuzrdgsuctlem  10566  climdm  11548  sum0  11641  isumz  11642  fsumsersdc  11648  isumclim  11674  zprodap0  11834  psrbaglesuppg  14376  iscnp3  14617  cnpnei  14633  cnclima  14637  cnrest2  14650  hmeores  14729  metcnp  14926  qtopbasss  14935  tgqioo  14969  dvaddxx  15117  dvmulxx  15118  dviaddf  15119  dvimulf  15120  dvef  15141  pilem3  15197