Theorem ffun 5513

Description: A mapping is a function. (Contributed by NM, 3-Aug-1994.)

Assertion

Ref	Expression
ffun	⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹)

Proof of Theorem ffun

Step	Hyp	Ref	Expression
1		ffn 5510	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnfun 5455	. 2 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
3	1, 2	syl 14	1 ⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹)

Syntax hints:   → wi 4  Fun wfun 5348   Fn wfn 5349  ⟶wf 5350

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 5357  df-f 5358

This theorem is referenced by:  ffund  5514  funssxp  5534  f00  5561  fofun  5593  fun11iun  5637  fimacnv  5808  dff3im  5824  resflem  5843  fmptco  5845  fliftf  5974  fsuppeq  6449  fsuppeqg  6450  smores2  6527  pmfun  6904  elmapfun  6908  pmresg  6912  ac6sfi  7157  ffsuppbi  7255  casef  7381  omp1eomlem  7387  ctm  7402  exmidfodomrlemim  7506  fcdmnn0fsuppg  9556  nn0supp  9557  frecuzrdg0  10782  frecuzrdgsuc  10783  frecuzrdgdomlem  10786  frecuzrdg0t  10791  frecuzrdgsuctlem  10792  climdm  11988  sum0  12082  isumz  12083  fsumsersdc  12089  isumclim  12115  zprodap0  12275  psrbaglesuppg  14870  iscnp3  15117  cnpnei  15133  cnclima  15137  cnrest2  15150  hmeores  15229  metcnp  15426  qtopbasss  15435  tgqioo  15469  dvaddxx  15617  dvmulxx  15618  dviaddf  15619  dvimulf  15620  dvef  15641  pilem3  15697  subusgr  16319  upgr2wlkdc  16421