Theorem ffun 5534

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

Syntax hints:   → wi 4  Fun wfun 5369   Fn wfn 5370  ⟶wf 5371

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 5378  df-f 5379

This theorem is referenced by:  ffund  5535  funssxp  5555  f00  5582  fofun  5614  fun11iun  5658  fimacnv  5831  dff3im  5847  resflem  5866  fmptco  5868  fliftf  5999  fsuppeq  6481  fsuppeqg  6482  smores2  6559  pmfun  6936  elmapfun  6947  pmresg  6951  ac6sfi  7196  ffsuppbi  7294  casef  7422  omp1eomlem  7428  ctm  7443  exmidfodomrlemim  7547  fcdmnn0fsuppg  9601  nn0supp  9602  frecuzrdg0  10833  frecuzrdgsuc  10834  frecuzrdgdomlem  10837  frecuzrdg0t  10842  frecuzrdgsuctlem  10843  climdm  12044  sum0  12138  isumz  12139  fsumsersdc  12145  isumclim  12171  zprodap0  12331  psrbaglesuppg  15040  iscnp3  15287  cnpnei  15303  cnclima  15307  cnrest2  15320  hmeores  15399  metcnp  15596  qtopbasss  15605  tgqioo  15639  dvaddxx  15787  dvmulxx  15788  dviaddf  15789  dvimulf  15790  dvef  15811  pilem3  15867  subusgr  16499  upgr2wlkdc  16601