Theorem ffun 5369

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

Syntax hints:   -> wi 4   Fun wfun 5211   Fn wfn 5212   -->wf 5213

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 5220  df-f 5221

This theorem is referenced by:  ffund  5370  funssxp  5386  f00  5408  fofun  5440  fun11iun  5483  fimacnv  5646  dff3im  5662  resflem  5681  fmptco  5683  fliftf  5800  smores2  6295  pmfun  6668  elmapfun  6672  pmresg  6676  ac6sfi  6898  casef  7087  omp1eomlem  7093  ctm  7108  exmidfodomrlemim  7200  nn0supp  9228  frecuzrdg0  10413  frecuzrdgsuc  10414  frecuzrdgdomlem  10417  frecuzrdg0t  10422  frecuzrdgsuctlem  10423  climdm  11303  sum0  11396  isumz  11397  fsumsersdc  11403  isumclim  11429  zprodap0  11589  iscnp3  13706  cnpnei  13722  cnclima  13726  cnrest2  13739  hmeores  13818  metcnp  14015  qtopbasss  14024  tgqioo  14050  dvaddxx  14170  dvmulxx  14171  dviaddf  14172  dvimulf  14173  dvef  14191  pilem3  14207