Theorem fnfund 6636

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

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

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 6539

This theorem is referenced by:  ffun  6708  f1fun  6776  imadrhmcl  20900  noseqrdg0  28500  noseqrdgsuc  28501  esplyind  33965  ply1degltdimlem  34012  bnj945  35162  bnj545  35283  bnj548  35285  bnj553  35286  bnj570  35293  bnj929  35324  bnj966  35332  bnj1442  35437  bnj1450  35438  bnj1501  35455  aks6d1c2lem4  42894  aks6d1c2  42897  aks6d1c6lem5  42944  eqresfnbd  43003  idemb  49937