Theorem ffun 5479

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

Syntax hints:   → wi 4  Fun wfun 5315   Fn wfn 5316  ⟶wf 5317

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 5324  df-f 5325

This theorem is referenced by:  ffund  5480  funssxp  5498  f00  5522  fofun  5554  fun11iun  5598  fimacnv  5769  dff3im  5785  resflem  5804  fmptco  5806  fliftf  5932  smores2  6451  pmfun  6828  elmapfun  6832  pmresg  6836  ac6sfi  7073  casef  7271  omp1eomlem  7277  ctm  7292  exmidfodomrlemim  7395  nn0supp  9437  frecuzrdg0  10652  frecuzrdgsuc  10653  frecuzrdgdomlem  10656  frecuzrdg0t  10661  frecuzrdgsuctlem  10662  climdm  11827  sum0  11920  isumz  11921  fsumsersdc  11927  isumclim  11953  zprodap0  12113  psrbaglesuppg  14657  iscnp3  14898  cnpnei  14914  cnclima  14918  cnrest2  14931  hmeores  15010  metcnp  15207  qtopbasss  15216  tgqioo  15250  dvaddxx  15398  dvmulxx  15399  dviaddf  15400  dvimulf  15401  dvef  15422  pilem3  15478  upgr2wlkdc  16147