Theorem ffun 5452

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

Syntax hints:   → wi 4  Fun wfun 5288   Fn wfn 5289  ⟶wf 5290

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 5297  df-f 5298

This theorem is referenced by:  ffund  5453  funssxp  5469  f00  5493  fofun  5525  fun11iun  5569  fimacnv  5737  dff3im  5753  resflem  5772  fmptco  5774  fliftf  5896  smores2  6410  pmfun  6785  elmapfun  6789  pmresg  6793  ac6sfi  7028  casef  7223  omp1eomlem  7229  ctm  7244  exmidfodomrlemim  7347  nn0supp  9389  frecuzrdg0  10602  frecuzrdgsuc  10603  frecuzrdgdomlem  10606  frecuzrdg0t  10611  frecuzrdgsuctlem  10612  climdm  11772  sum0  11865  isumz  11866  fsumsersdc  11872  isumclim  11898  zprodap0  12058  psrbaglesuppg  14601  iscnp3  14842  cnpnei  14858  cnclima  14862  cnrest2  14875  hmeores  14954  metcnp  15151  qtopbasss  15160  tgqioo  15194  dvaddxx  15342  dvmulxx  15343  dviaddf  15344  dvimulf  15345  dvef  15366  pilem3  15422