Theorem fnfund 6590

Description: A function with domain is a function, deduction form. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypothesis

Ref	Expression
fnfund.1	⊢ (𝜑 → 𝐹 Fn 𝐴)

Assertion

Ref	Expression
fnfund	⊢ (𝜑 → Fun 𝐹)

Proof of Theorem fnfund

Step	Hyp	Ref	Expression
1		fnfund.1	. 2 ⊢ (𝜑 → 𝐹 Fn 𝐴)
2		fnfun 6589	. 2 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
3	1, 2	syl 17	1 ⊢ (𝜑 → Fun 𝐹)

Syntax hints:   → wi 4  Fun wfun 6483   Fn wfn 6484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-fn 6492

This theorem is referenced by:  imadrhmcl  20721  noseqrdg0  28257  noseqrdgsuc  28258  esplyind  33659  ply1degltdimlem  33707  bnj945  34857  bnj545  34979  bnj548  34981  bnj553  34982  bnj570  34989  bnj929  35020  bnj966  35028  bnj1442  35133  bnj1450  35134  bnj1501  35151  aks6d1c2lem4  42293  aks6d1c2  42296  aks6d1c6lem5  42343  eqresfnbd  42403  idemb  49320