Theorem ffun 5073

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

Syntax hints:   → wi 4  Fun wfun 4920   Fn wfn 4921  ⟶wf 4922

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

This theorem depends on definitions:  df-bi 115  df-fn 4929  df-f 4930

This theorem is referenced by:  funssxp  5085  f00  5106  fofun  5132  fun11iun  5172  fimacnv  5322  dff3im  5338  fmptco  5356  fliftf  5464  smores2  5937  ac6sfi  6421  nn0supp  8396  frecuzrdg0  9484  frecuzrdgsuc  9485  frecuzrdgdomlem  9488  frecuzrdg0t  9493  frecuzrdgsuctlem  9494  climdm  10261