Theorem ffun 5370

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

Syntax hints:   → wi 4  Fun wfun 5212   Fn wfn 5213  ⟶wf 5214

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 5221  df-f 5222

This theorem is referenced by:  ffund  5371  funssxp  5387  f00  5409  fofun  5441  fun11iun  5484  fimacnv  5647  dff3im  5663  resflem  5682  fmptco  5684  fliftf  5802  smores2  6297  pmfun  6670  elmapfun  6674  pmresg  6678  ac6sfi  6900  casef  7089  omp1eomlem  7095  ctm  7110  exmidfodomrlemim  7202  nn0supp  9230  frecuzrdg0  10415  frecuzrdgsuc  10416  frecuzrdgdomlem  10419  frecuzrdg0t  10424  frecuzrdgsuctlem  10425  climdm  11305  sum0  11398  isumz  11399  fsumsersdc  11405  isumclim  11431  zprodap0  11591  iscnp3  13742  cnpnei  13758  cnclima  13762  cnrest2  13775  hmeores  13854  metcnp  14051  qtopbasss  14060  tgqioo  14086  dvaddxx  14206  dvmulxx  14207  dviaddf  14208  dvimulf  14209  dvef  14227  pilem3  14243