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  9622  nn0supp  9623  frecuzrdg0  10863  frecuzrdgsuc  10864  frecuzrdgdomlem  10867  frecuzrdg0t  10872  frecuzrdgsuctlem  10873  climdm  12077  sum0  12171  isumz  12172  fsumsersdc  12178  isumclim  12204  zprodap0  12364  psrbaglesuppg  15106  iscnp3  15353  cnpnei  15369  cnclima  15373  cnrest2  15386  hmeores  15465  metcnp  15662  qtopbasss  15671  tgqioo  15705  dvaddxx  15853  dvmulxx  15854  dviaddf  15855  dvimulf  15856  dvef  15877  pilem3  15934  subusgr  16614  upgr2wlkdc  16716