Theorem ffun 5531

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

Syntax hints:   -> wi 4   Fun wfun 5366   Fn wfn 5367   -->wf 5368

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 5375  df-f 5376

This theorem is referenced by:  ffund  5532  funssxp  5552  f00  5579  fofun  5611  fun11iun  5655  fimacnv  5828  dff3im  5844  resflem  5863  fmptco  5865  fliftf  5995  fsuppeq  6477  fsuppeqg  6478  smores2  6555  pmfun  6932  elmapfun  6943  pmresg  6947  ac6sfi  7192  ffsuppbi  7290  casef  7418  omp1eomlem  7424  ctm  7439  exmidfodomrlemim  7543  fcdmnn0fsuppg  9597  nn0supp  9598  frecuzrdg0  10828  frecuzrdgsuc  10829  frecuzrdgdomlem  10832  frecuzrdg0t  10837  frecuzrdgsuctlem  10838  climdm  12039  sum0  12133  isumz  12134  fsumsersdc  12140  isumclim  12166  zprodap0  12326  psrbaglesuppg  14980  iscnp3  15227  cnpnei  15243  cnclima  15247  cnrest2  15260  hmeores  15339  metcnp  15536  qtopbasss  15545  tgqioo  15579  dvaddxx  15727  dvmulxx  15728  dviaddf  15729  dvimulf  15730  dvef  15751  pilem3  15807  subusgr  16430  upgr2wlkdc  16532