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  7428  omp1eomlem  7434  ctm  7449  exmidfodomrlemim  7553  fcdmnn0fsuppg  9618  nn0supp  9619  frecuzrdg0  10850  frecuzrdgsuc  10851  frecuzrdgdomlem  10854  frecuzrdg0t  10859  frecuzrdgsuctlem  10860  climdm  12061  sum0  12155  isumz  12156  fsumsersdc  12162  isumclim  12188  zprodap0  12348  psrbaglesuppg  15057  iscnp3  15304  cnpnei  15320  cnclima  15324  cnrest2  15337  hmeores  15416  metcnp  15613  qtopbasss  15622  tgqioo  15656  dvaddxx  15804  dvmulxx  15805  dviaddf  15806  dvimulf  15807  dvef  15828  pilem3  15884  subusgr  16516  upgr2wlkdc  16618