Theorem ffun 5434

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

Syntax hints:   → wi 4  Fun wfun 5270   Fn wfn 5271  ⟶wf 5272

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 5279  df-f 5280

This theorem is referenced by:  ffund  5435  funssxp  5451  f00  5474  fofun  5506  fun11iun  5550  fimacnv  5716  dff3im  5732  resflem  5751  fmptco  5753  fliftf  5875  smores2  6387  pmfun  6762  elmapfun  6766  pmresg  6770  ac6sfi  7002  casef  7197  omp1eomlem  7203  ctm  7218  exmidfodomrlemim  7316  nn0supp  9354  frecuzrdg0  10565  frecuzrdgsuc  10566  frecuzrdgdomlem  10569  frecuzrdg0t  10574  frecuzrdgsuctlem  10575  climdm  11650  sum0  11743  isumz  11744  fsumsersdc  11750  isumclim  11776  zprodap0  11936  psrbaglesuppg  14478  iscnp3  14719  cnpnei  14735  cnclima  14739  cnrest2  14752  hmeores  14831  metcnp  15028  qtopbasss  15037  tgqioo  15071  dvaddxx  15219  dvmulxx  15220  dviaddf  15221  dvimulf  15222  dvef  15243  pilem3  15299