Theorem fnfund 6640

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

This proof depends on syntax axioms:   → wi 4  Fun wfun 6534   Fn wfn 6535

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fn 6543

This theorem is used by:  ffun  6712  f1fun  6780  imadrhmcl  20952  noseqrdg0  28553  noseqrdgsuc  28554  esplyind  34031  ply1degltdimlem  34078  bnj945  35229  bnj545  35350  bnj548  35352  bnj553  35353  bnj570  35360  bnj929  35391  bnj966  35399  bnj1442  35504  bnj1450  35505  bnj1501  35522  aks6d1c2lem4  42954  aks6d1c2  42957  aks6d1c6lem5  43004  eqresfnbd  43063  idemb  49996