Theorem ffun 5487

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 5484	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnfun 5429	. 2 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
3	1, 2	syl 14	1 ⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹)

Syntax hints:   → wi 4  Fun wfun 5322   Fn wfn 5323  ⟶wf 5324

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 5331  df-f 5332

This theorem is referenced by:  ffund  5488  funssxp  5506  f00  5531  fofun  5563  fun11iun  5607  fimacnv  5779  dff3im  5795  resflem  5814  fmptco  5816  fliftf  5945  smores2  6465  pmfun  6842  elmapfun  6846  pmresg  6850  ac6sfi  7092  casef  7292  omp1eomlem  7298  ctm  7313  exmidfodomrlemim  7417  nn0supp  9459  frecuzrdg0  10681  frecuzrdgsuc  10682  frecuzrdgdomlem  10685  frecuzrdg0t  10690  frecuzrdgsuctlem  10691  climdm  11878  sum0  11972  isumz  11973  fsumsersdc  11979  isumclim  12005  zprodap0  12165  psrbaglesuppg  14710  iscnp3  14956  cnpnei  14972  cnclima  14976  cnrest2  14989  hmeores  15068  metcnp  15265  qtopbasss  15274  tgqioo  15308  dvaddxx  15456  dvmulxx  15457  dviaddf  15458  dvimulf  15459  dvef  15480  pilem3  15536  subusgr  16155  upgr2wlkdc  16257