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  5940  smores2  6460  pmfun  6837  elmapfun  6841  pmresg  6845  ac6sfi  7087  casef  7287  omp1eomlem  7293  ctm  7308  exmidfodomrlemim  7412  nn0supp  9454  frecuzrdg0  10676  frecuzrdgsuc  10677  frecuzrdgdomlem  10680  frecuzrdg0t  10685  frecuzrdgsuctlem  10686  climdm  11860  sum0  11954  isumz  11955  fsumsersdc  11961  isumclim  11987  zprodap0  12147  psrbaglesuppg  14692  iscnp3  14933  cnpnei  14949  cnclima  14953  cnrest2  14966  hmeores  15045  metcnp  15242  qtopbasss  15251  tgqioo  15285  dvaddxx  15433  dvmulxx  15434  dviaddf  15435  dvimulf  15436  dvef  15457  pilem3  15513  subusgr  16132  upgr2wlkdc  16234