Theorem ffun 5516

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

Syntax hints:   -> wi 4   Fun wfun 5351   Fn wfn 5352   -->wf 5353

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 5360  df-f 5361

This theorem is referenced by:  ffund  5517  funssxp  5537  f00  5564  fofun  5596  fun11iun  5640  fimacnv  5811  dff3im  5827  resflem  5846  fmptco  5848  fliftf  5978  fsuppeq  6460  fsuppeqg  6461  smores2  6538  pmfun  6915  elmapfun  6919  pmresg  6923  ac6sfi  7168  ffsuppbi  7266  casef  7392  omp1eomlem  7398  ctm  7413  exmidfodomrlemim  7517  fcdmnn0fsuppg  9568  nn0supp  9569  frecuzrdg0  10799  frecuzrdgsuc  10800  frecuzrdgdomlem  10803  frecuzrdg0t  10808  frecuzrdgsuctlem  10809  climdm  12005  sum0  12099  isumz  12100  fsumsersdc  12106  isumclim  12132  zprodap0  12292  psrbaglesuppg  14947  iscnp3  15194  cnpnei  15210  cnclima  15214  cnrest2  15227  hmeores  15306  metcnp  15503  qtopbasss  15512  tgqioo  15546  dvaddxx  15694  dvmulxx  15695  dviaddf  15696  dvimulf  15697  dvef  15718  pilem3  15774  subusgr  16396  upgr2wlkdc  16498