Theorem ffun 5492

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

Syntax hints:   -> wi 4   Fun wfun 5327   Fn wfn 5328   -->wf 5329

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 5336  df-f 5337

This theorem is referenced by:  ffund  5493  funssxp  5512  f00  5537  fofun  5569  fun11iun  5613  fimacnv  5784  dff3im  5800  resflem  5819  fmptco  5821  fliftf  5950  fsuppeq  6425  fsuppeqg  6426  smores2  6503  pmfun  6880  elmapfun  6884  pmresg  6888  ac6sfi  7130  casef  7330  omp1eomlem  7336  ctm  7351  exmidfodomrlemim  7455  nn0supp  9498  frecuzrdg0  10721  frecuzrdgsuc  10722  frecuzrdgdomlem  10725  frecuzrdg0t  10730  frecuzrdgsuctlem  10731  climdm  11918  sum0  12012  isumz  12013  fsumsersdc  12019  isumclim  12045  zprodap0  12205  psrbaglesuppg  14751  iscnp3  14997  cnpnei  15013  cnclima  15017  cnrest2  15030  hmeores  15109  metcnp  15306  qtopbasss  15315  tgqioo  15349  dvaddxx  15497  dvmulxx  15498  dviaddf  15499  dvimulf  15500  dvef  15521  pilem3  15577  subusgr  16199  upgr2wlkdc  16301