Theorem fnfund 6599

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

Syntax hints:   → wi 4  Fun wfun 6492   Fn wfn 6493

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 6501

This theorem is referenced by:  imadrhmcl  20774  noseqrdg0  28299  noseqrdgsuc  28300  esplyind  33719  ply1degltdimlem  33766  bnj945  34916  bnj545  35037  bnj548  35039  bnj553  35040  bnj570  35047  bnj929  35078  bnj966  35086  bnj1442  35191  bnj1450  35192  bnj1501  35209  aks6d1c2lem4  42566  aks6d1c2  42569  aks6d1c6lem5  42616  eqresfnbd  42673  idemb  49634