Theorem ffun 5516

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

Syntax hints:   → wi 4  Fun wfun 5351   Fn wfn 5352  ⟶wf 5353

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 5360  df-f 5361

This theorem is referenced by:  ffund  5517  funssxp  5537  f00  5564  fofun  5596  fun11iun  5640  fimacnv  5811  dff3im  5827  resflem  5846  fmptco  5848  fliftf  5978  fsuppeq  6460  fsuppeqg  6461  smores2  6538  pmfun  6915  elmapfun  6919  pmresg  6923  ac6sfi  7168  ffsuppbi  7266  casef  7392  omp1eomlem  7398  ctm  7413  exmidfodomrlemim  7517  fcdmnn0fsuppg  9571  nn0supp  9572  frecuzrdg0  10802  frecuzrdgsuc  10803  frecuzrdgdomlem  10806  frecuzrdg0t  10811  frecuzrdgsuctlem  10812  climdm  12008  sum0  12102  isumz  12103  fsumsersdc  12109  isumclim  12135  zprodap0  12295  psrbaglesuppg  14950  iscnp3  15197  cnpnei  15213  cnclima  15217  cnrest2  15230  hmeores  15309  metcnp  15506  qtopbasss  15515  tgqioo  15549  dvaddxx  15697  dvmulxx  15698  dviaddf  15699  dvimulf  15700  dvef  15721  pilem3  15777  subusgr  16399  upgr2wlkdc  16501