Theorem ffun 5233

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

Syntax hints:   → wi 4  Fun wfun 5075   Fn wfn 5076  ⟶wf 5077

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-fn 5084  df-f 5085

This theorem is referenced by:  ffund  5234  funssxp  5250  f00  5272  fofun  5304  fun11iun  5344  fimacnv  5503  dff3im  5519  resflem  5538  fmptco  5540  fliftf  5654  smores2  6145  pmfun  6516  elmapfun  6520  pmresg  6524  ac6sfi  6745  casef  6925  omp1eomlem  6931  ctm  6946  exmidfodomrlemim  7005  nn0supp  8933  frecuzrdg0  10079  frecuzrdgsuc  10080  frecuzrdgdomlem  10083  frecuzrdg0t  10088  frecuzrdgsuctlem  10089  climdm  10956  sum0  11049  isumz  11050  fsumsersdc  11056  isumclim  11082  iscnp3  12214  cnpnei  12230  cnclima  12234  cnrest2  12247  metcnp  12501  qtopbasss  12510  tgqioo  12533  dvaddxx  12622  dvmulxx  12623  dviaddf  12624  dvimulf  12625