Theorem ffun 5476

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

Syntax hints:   → wi 4  Fun wfun 5312   Fn wfn 5313  ⟶wf 5314

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 5321  df-f 5322

This theorem is referenced by:  ffund  5477  funssxp  5495  f00  5519  fofun  5551  fun11iun  5595  fimacnv  5766  dff3im  5782  resflem  5801  fmptco  5803  fliftf  5929  smores2  6446  pmfun  6823  elmapfun  6827  pmresg  6831  ac6sfi  7068  casef  7263  omp1eomlem  7269  ctm  7284  exmidfodomrlemim  7387  nn0supp  9429  frecuzrdg0  10643  frecuzrdgsuc  10644  frecuzrdgdomlem  10647  frecuzrdg0t  10652  frecuzrdgsuctlem  10653  climdm  11814  sum0  11907  isumz  11908  fsumsersdc  11914  isumclim  11940  zprodap0  12100  psrbaglesuppg  14644  iscnp3  14885  cnpnei  14901  cnclima  14905  cnrest2  14918  hmeores  14997  metcnp  15194  qtopbasss  15203  tgqioo  15237  dvaddxx  15385  dvmulxx  15386  dviaddf  15387  dvimulf  15388  dvef  15409  pilem3  15465  upgr2wlkdc  16096