Theorem ffun 5348

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

Syntax hints:   -> wi 4   Fun wfun 5190   Fn wfn 5191   -->wf 5192

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-fn 5199  df-f 5200

This theorem is referenced by:  ffund  5349  funssxp  5365  f00  5387  fofun  5419  fun11iun  5461  fimacnv  5622  dff3im  5638  resflem  5657  fmptco  5659  fliftf  5775  smores2  6270  pmfun  6642  elmapfun  6646  pmresg  6650  ac6sfi  6872  casef  7061  omp1eomlem  7067  ctm  7082  exmidfodomrlemim  7165  nn0supp  9174  frecuzrdg0  10356  frecuzrdgsuc  10357  frecuzrdgdomlem  10360  frecuzrdg0t  10365  frecuzrdgsuctlem  10366  climdm  11245  sum0  11338  isumz  11339  fsumsersdc  11345  isumclim  11371  zprodap0  11531  iscnp3  12918  cnpnei  12934  cnclima  12938  cnrest2  12951  hmeores  13030  metcnp  13227  qtopbasss  13236  tgqioo  13262  dvaddxx  13382  dvmulxx  13383  dviaddf  13384  dvimulf  13385  dvef  13403  pilem3  13419