Theorem ffun 5350

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

Syntax hints:   → wi 4  Fun wfun 5192   Fn wfn 5193  ⟶wf 5194

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-fn 5201  df-f 5202

This theorem is referenced by:  ffund  5351  funssxp  5367  f00  5389  fofun  5421  fun11iun  5463  fimacnv  5625  dff3im  5641  resflem  5660  fmptco  5662  fliftf  5778  smores2  6273  pmfun  6646  elmapfun  6650  pmresg  6654  ac6sfi  6876  casef  7065  omp1eomlem  7071  ctm  7086  exmidfodomrlemim  7178  nn0supp  9187  frecuzrdg0  10369  frecuzrdgsuc  10370  frecuzrdgdomlem  10373  frecuzrdg0t  10378  frecuzrdgsuctlem  10379  climdm  11258  sum0  11351  isumz  11352  fsumsersdc  11358  isumclim  11384  zprodap0  11544  iscnp3  12997  cnpnei  13013  cnclima  13017  cnrest2  13030  hmeores  13109  metcnp  13306  qtopbasss  13315  tgqioo  13341  dvaddxx  13461  dvmulxx  13462  dviaddf  13463  dvimulf  13464  dvef  13482  pilem3  13498