Theorem fnfund 6586

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

Syntax hints:   → wi 4  Fun wfun 6479   Fn wfn 6480

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 208  df-an 397  df-fn 6488

This theorem is referenced by:  imadrhmcl  20769  noseqrdg0  28317  noseqrdgsuc  28318  esplyind  33759  ply1degltdimlem  33806  bnj945  34956  bnj545  35077  bnj548  35079  bnj553  35080  bnj570  35087  bnj929  35118  bnj966  35126  bnj1442  35231  bnj1450  35232  bnj1501  35249  aks6d1c2lem4  42612  aks6d1c2  42615  aks6d1c6lem5  42662  eqresfnbd  42719  idemb  49649