Theorem ffun 5510

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

Syntax hints:   → wi 4  Fun wfun 5345   Fn wfn 5346  ⟶wf 5347

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 5354  df-f 5355

This theorem is referenced by:  ffund  5511  funssxp  5531  f00  5558  fofun  5590  fun11iun  5634  fimacnv  5805  dff3im  5821  resflem  5840  fmptco  5842  fliftf  5971  fsuppeq  6446  fsuppeqg  6447  smores2  6524  pmfun  6901  elmapfun  6905  pmresg  6909  ac6sfi  7154  ffsuppbi  7252  casef  7378  omp1eomlem  7384  ctm  7399  exmidfodomrlemim  7503  fcdmnn0fsuppg  9547  nn0supp  9548  frecuzrdg0  10771  frecuzrdgsuc  10772  frecuzrdgdomlem  10775  frecuzrdg0t  10780  frecuzrdgsuctlem  10781  climdm  11973  sum0  12067  isumz  12068  fsumsersdc  12074  isumclim  12100  zprodap0  12260  psrbaglesuppg  14808  iscnp3  15055  cnpnei  15071  cnclima  15075  cnrest2  15088  hmeores  15167  metcnp  15364  qtopbasss  15373  tgqioo  15407  dvaddxx  15555  dvmulxx  15556  dviaddf  15557  dvimulf  15558  dvef  15579  pilem3  15635  subusgr  16257  upgr2wlkdc  16359