Theorem fnfund 6601

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

Syntax hints:   → wi 4  Fun wfun 6494   Fn wfn 6495

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 6503

This theorem is referenced by:  imadrhmcl  20742  noseqrdg0  28315  noseqrdgsuc  28316  esplyind  33752  ply1degltdimlem  33800  bnj945  34950  bnj545  35071  bnj548  35073  bnj553  35074  bnj570  35081  bnj929  35112  bnj966  35120  bnj1442  35225  bnj1450  35226  bnj1501  35243  aks6d1c2lem4  42497  aks6d1c2  42500  aks6d1c6lem5  42547  eqresfnbd  42604  idemb  49518