Theorem ffun 5539

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 5536	. 2 |- ( F : A --> B -> F Fn A )
2		fnfun 5481	. 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 5374   Fn wfn 5375   -->wf 5376

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 5383  df-f 5384

This theorem is used by:  ffund  5540  funssxp  5560  f00  5587  fofun  5619  fun11iun  5663  fimacnv  5840  dff3im  5856  resflem  5875  fmptco  5877  fliftf  6008  fsuppeq  6491  fsuppeqg  6492  smores2  6569  pmfun  6946  elmapfun  6957  pmresg  6961  ac6sfi  7206  ffsuppbi  7305  casef  7434  omp1eomlem  7440  ctm  7455  exmidfodomrlemim  7559  fcdmnn0fsuppg  9629  nn0supp  9630  frecuzrdg0  10871  frecuzrdgsuc  10872  frecuzrdgdomlem  10875  frecuzrdg0t  10880  frecuzrdgsuctlem  10881  climdm  12086  sum0  12180  isumz  12181  fsumsersdc  12187  isumclim  12213  zprodap0  12373  psrbaglesuppg  15166  iscnp3  15429  cnpnei  15445  cnclima  15449  cnrest2  15462  hmeores  15541  metcnp  15738  qtopbasss  15747  tgqioo  15781  dvaddxx  15929  dvmulxx  15930  dviaddf  15931  dvimulf  15932  dvef  15953  pilem3  16010  subusgr  16721  upgr2wlkdc  16823