Theorem ffun 5536

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

This proof depends on syntax axioms:   -> wi 4   Fun wfun 5371   Fn wfn 5372   -->wf 5373

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-fn 5380  df-f 5381

This theorem is used by:  ffund  5537  funssxp  5557  f00  5584  fofun  5616  fun11iun  5660  fimacnv  5837  dff3im  5853  resflem  5872  fmptco  5874  fliftf  6005  fsuppeq  6487  fsuppeqg  6488  smores2  6565  pmfun  6942  elmapfun  6953  pmresg  6957  ac6sfi  7202  ffsuppbi  7300  casef  7429  omp1eomlem  7435  ctm  7450  exmidfodomrlemim  7554  fcdmnn0fsuppg  9623  nn0supp  9624  frecuzrdg0  10865  frecuzrdgsuc  10866  frecuzrdgdomlem  10869  frecuzrdg0t  10874  frecuzrdgsuctlem  10875  climdm  12080  sum0  12174  isumz  12175  fsumsersdc  12181  isumclim  12207  zprodap0  12367  psrbaglesuppg  15141  iscnp3  15395  cnpnei  15411  cnclima  15415  cnrest2  15428  hmeores  15507  metcnp  15704  qtopbasss  15713  tgqioo  15747  dvaddxx  15895  dvmulxx  15896  dviaddf  15897  dvimulf  15898  dvef  15919  pilem3  15976  subusgr  16682  upgr2wlkdc  16784