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  11577  sum0  11670  isumz  11671  fsumsersdc  11677  isumclim  11703  zprodap0  11863  psrbaglesuppg  14405  iscnp3  14646  cnpnei  14662  cnclima  14666  cnrest2  14679  hmeores  14758  metcnp  14955  qtopbasss  14964  tgqioo  14998  dvaddxx  15146  dvmulxx  15147  dviaddf  15148  dvimulf  15149  dvef  15170  pilem3  15226