Theorem fnfund 6594

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

Syntax hints:   → wi 4  Fun wfun 6487   Fn wfn 6488

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 6496

This theorem is referenced by:  imadrhmcl  20768  noseqrdg0  28316  noseqrdgsuc  28317  esplyind  33737  ply1degltdimlem  33785  bnj945  34935  bnj545  35056  bnj548  35058  bnj553  35059  bnj570  35066  bnj929  35097  bnj966  35105  bnj1442  35210  bnj1450  35211  bnj1501  35228  aks6d1c2lem4  42583  aks6d1c2  42586  aks6d1c6lem5  42633  eqresfnbd  42690  idemb  49649