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  6570  pmfun  6947  elmapfun  6958  pmresg  6962  ac6sfi  7208  casef  7434  omp1eomlem  7440  ctm  7455  exmidfodomrlemim  7559  nn0supp  9628  frecuzrdg0  10870  frecuzrdgsuc  10871  frecuzrdgdomlem  10874  frecuzrdg0t  10879  frecuzrdgsuctlem  10880  climdm  12085  sum0  12179  isumz  12180  fsumsersdc  12186  isumclim  12212  zprodap0  12372  psrbaglesuppg  15170  iscnp3  15446  cnpnei  15462  cnclima  15466  cnrest2  15479  hmeores  15558  metcnp  15755  qtopbasss  15764  tgqioo  15798  dvaddxx  15946  dvmulxx  15947  dviaddf  15948  dvimulf  15949  dvef  15970  pilem3  16027  subusgr  16738  upgr2wlkdc  16840