Theorem ffun 5485

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

Syntax hints:   → wi 4  Fun wfun 5320   Fn wfn 5321  ⟶wf 5322

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 5329  df-f 5330

This theorem is referenced by:  ffund  5486  funssxp  5504  f00  5528  fofun  5560  fun11iun  5604  fimacnv  5776  dff3im  5792  resflem  5811  fmptco  5813  fliftf  5940  smores2  6460  pmfun  6837  elmapfun  6841  pmresg  6845  ac6sfi  7087  casef  7287  omp1eomlem  7293  ctm  7308  exmidfodomrlemim  7412  nn0supp  9454  frecuzrdg0  10676  frecuzrdgsuc  10677  frecuzrdgdomlem  10680  frecuzrdg0t  10685  frecuzrdgsuctlem  10686  climdm  11857  sum0  11951  isumz  11952  fsumsersdc  11958  isumclim  11984  zprodap0  12144  psrbaglesuppg  14689  iscnp3  14930  cnpnei  14946  cnclima  14950  cnrest2  14963  hmeores  15042  metcnp  15239  qtopbasss  15248  tgqioo  15282  dvaddxx  15430  dvmulxx  15431  dviaddf  15432  dvimulf  15433  dvef  15454  pilem3  15510  subusgr  16129  upgr2wlkdc  16231