Theorem ffun 5270

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

Syntax hints:   → wi 4  Fun wfun 5112   Fn wfn 5113  ⟶wf 5114

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 5121  df-f 5122

This theorem is referenced by:  ffund  5271  funssxp  5287  f00  5309  fofun  5341  fun11iun  5381  fimacnv  5542  dff3im  5558  resflem  5577  fmptco  5579  fliftf  5693  smores2  6184  pmfun  6555  elmapfun  6559  pmresg  6563  ac6sfi  6785  casef  6966  omp1eomlem  6972  ctm  6987  exmidfodomrlemim  7050  nn0supp  9022  frecuzrdg0  10179  frecuzrdgsuc  10180  frecuzrdgdomlem  10183  frecuzrdg0t  10188  frecuzrdgsuctlem  10189  climdm  11057  sum0  11150  isumz  11151  fsumsersdc  11157  isumclim  11183  iscnp3  12361  cnpnei  12377  cnclima  12381  cnrest2  12394  hmeores  12473  metcnp  12670  qtopbasss  12679  tgqioo  12705  dvaddxx  12825  dvmulxx  12826  dviaddf  12827  dvimulf  12828  dvef  12845  pilem3  12853