Theorem ffun 5482

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

Syntax hints:   → wi 4  Fun wfun 5318   Fn wfn 5319  ⟶wf 5320

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 5327  df-f 5328

This theorem is referenced by:  ffund  5483  funssxp  5501  f00  5525  fofun  5557  fun11iun  5601  fimacnv  5772  dff3im  5788  resflem  5807  fmptco  5809  fliftf  5935  smores2  6455  pmfun  6832  elmapfun  6836  pmresg  6840  ac6sfi  7082  casef  7281  omp1eomlem  7287  ctm  7302  exmidfodomrlemim  7405  nn0supp  9447  frecuzrdg0  10668  frecuzrdgsuc  10669  frecuzrdgdomlem  10672  frecuzrdg0t  10677  frecuzrdgsuctlem  10678  climdm  11849  sum0  11942  isumz  11943  fsumsersdc  11949  isumclim  11975  zprodap0  12135  psrbaglesuppg  14679  iscnp3  14920  cnpnei  14936  cnclima  14940  cnrest2  14953  hmeores  15032  metcnp  15229  qtopbasss  15238  tgqioo  15272  dvaddxx  15420  dvmulxx  15421  dviaddf  15422  dvimulf  15423  dvef  15444  pilem3  15500  upgr2wlkdc  16186