Theorem ffun 5275

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

Syntax hints:   -> wi 4   Fun wfun 5117   Fn wfn 5118   -->wf 5119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-fn 5126  df-f 5127

This theorem is referenced by:  ffund  5276  funssxp  5292  f00  5314  fofun  5346  fun11iun  5388  fimacnv  5549  dff3im  5565  resflem  5584  fmptco  5586  fliftf  5700  smores2  6191  pmfun  6562  elmapfun  6566  pmresg  6570  ac6sfi  6792  casef  6973  omp1eomlem  6979  ctm  6994  exmidfodomrlemim  7057  nn0supp  9029  frecuzrdg0  10186  frecuzrdgsuc  10187  frecuzrdgdomlem  10190  frecuzrdg0t  10195  frecuzrdgsuctlem  10196  climdm  11064  sum0  11157  isumz  11158  fsumsersdc  11164  isumclim  11190  iscnp3  12372  cnpnei  12388  cnclima  12392  cnrest2  12405  hmeores  12484  metcnp  12681  qtopbasss  12690  tgqioo  12716  dvaddxx  12836  dvmulxx  12837  dviaddf  12838  dvimulf  12839  dvef  12856  pilem3  12864