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  15148  iscnp3  15403  cnpnei  15419  cnclima  15423  cnrest2  15436  hmeores  15515  metcnp  15712  qtopbasss  15721  tgqioo  15755  dvaddxx  15903  dvmulxx  15904  dviaddf  15905  dvimulf  15906  dvef  15927  pilem3  15984  subusgr  16695  upgr2wlkdc  16797