Theorem ffun 5511

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

Syntax hints:   -> wi 4   Fun wfun 5346   Fn wfn 5347   -->wf 5348

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 5355  df-f 5356

This theorem is referenced by:  ffund  5512  funssxp  5532  f00  5559  fofun  5591  fun11iun  5635  fimacnv  5806  dff3im  5822  resflem  5841  fmptco  5843  fliftf  5972  fsuppeq  6447  fsuppeqg  6448  smores2  6525  pmfun  6902  elmapfun  6906  pmresg  6910  ac6sfi  7155  ffsuppbi  7253  casef  7379  omp1eomlem  7385  ctm  7400  exmidfodomrlemim  7504  fcdmnn0fsuppg  9551  nn0supp  9552  frecuzrdg0  10775  frecuzrdgsuc  10776  frecuzrdgdomlem  10779  frecuzrdg0t  10784  frecuzrdgsuctlem  10785  climdm  11980  sum0  12074  isumz  12075  fsumsersdc  12081  isumclim  12107  zprodap0  12267  psrbaglesuppg  14821  iscnp3  15068  cnpnei  15084  cnclima  15088  cnrest2  15101  hmeores  15180  metcnp  15377  qtopbasss  15386  tgqioo  15420  dvaddxx  15568  dvmulxx  15569  dviaddf  15570  dvimulf  15571  dvef  15592  pilem3  15648  subusgr  16270  upgr2wlkdc  16372