Theorem fnfund 6637

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 6636	. 2 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
3	1, 2	syl 18	1 ⊢ (𝜑 → Fun 𝐹)

Syntax hints:   → wi 4  Fun wfun 6531   Fn wfn 6532

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 210  df-an 401  df-fn 6540

This theorem is referenced by:  ffun  6709  f1fun  6777  imadrhmcl  20877  noseqrdg0  28465  noseqrdgsuc  28466  esplyind  33909  ply1degltdimlem  33956  bnj945  35106  bnj545  35227  bnj548  35229  bnj553  35230  bnj570  35237  bnj929  35268  bnj966  35276  bnj1442  35381  bnj1450  35382  bnj1501  35399  aks6d1c2lem4  42783  aks6d1c2  42786  aks6d1c6lem5  42833  eqresfnbd  42892  idemb  49821