Theorem ffun 5413

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

Syntax hints:   → wi 4  Fun wfun 5253   Fn wfn 5254  ⟶wf 5255

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 5262  df-f 5263

This theorem is referenced by:  ffund  5414  funssxp  5430  f00  5452  fofun  5484  fun11iun  5528  fimacnv  5694  dff3im  5710  resflem  5729  fmptco  5731  fliftf  5849  smores2  6361  pmfun  6736  elmapfun  6740  pmresg  6744  ac6sfi  6968  casef  7163  omp1eomlem  7169  ctm  7184  exmidfodomrlemim  7282  nn0supp  9320  frecuzrdg0  10524  frecuzrdgsuc  10525  frecuzrdgdomlem  10528  frecuzrdg0t  10533  frecuzrdgsuctlem  10534  climdm  11479  sum0  11572  isumz  11573  fsumsersdc  11579  isumclim  11605  zprodap0  11765  psrbaglesuppg  14304  iscnp3  14525  cnpnei  14541  cnclima  14545  cnrest2  14558  hmeores  14637  metcnp  14834  qtopbasss  14843  tgqioo  14877  dvaddxx  15025  dvmulxx  15026  dviaddf  15027  dvimulf  15028  dvef  15049  pilem3  15105