Theorem ffun 5485

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

Syntax hints:   -> wi 4   Fun wfun 5320   Fn wfn 5321   -->wf 5322

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 5329  df-f 5330

This theorem is referenced by:  ffund  5486  funssxp  5504  f00  5528  fofun  5560  fun11iun  5604  fimacnv  5776  dff3im  5792  resflem  5811  fmptco  5813  fliftf  5939  smores2  6459  pmfun  6836  elmapfun  6840  pmresg  6844  ac6sfi  7086  casef  7286  omp1eomlem  7292  ctm  7307  exmidfodomrlemim  7411  nn0supp  9453  frecuzrdg0  10674  frecuzrdgsuc  10675  frecuzrdgdomlem  10678  frecuzrdg0t  10683  frecuzrdgsuctlem  10684  climdm  11855  sum0  11948  isumz  11949  fsumsersdc  11955  isumclim  11981  zprodap0  12141  psrbaglesuppg  14685  iscnp3  14926  cnpnei  14942  cnclima  14946  cnrest2  14959  hmeores  15038  metcnp  15235  qtopbasss  15244  tgqioo  15278  dvaddxx  15426  dvmulxx  15427  dviaddf  15428  dvimulf  15429  dvef  15450  pilem3  15506  subusgr  16125  upgr2wlkdc  16227