Theorem fnfund 6593

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

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

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 6495

This theorem is referenced by:  imadrhmcl  20730  noseqrdg0  28303  noseqrdgsuc  28304  esplyind  33731  ply1degltdimlem  33779  bnj945  34929  bnj545  35051  bnj548  35053  bnj553  35054  bnj570  35061  bnj929  35092  bnj966  35100  bnj1442  35205  bnj1450  35206  bnj1501  35223  aks6d1c2lem4  42381  aks6d1c2  42384  aks6d1c6lem5  42431  eqresfnbd  42488  idemb  49404