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  20765  noseqrdg0  28313  noseqrdgsuc  28314  esplyind  33734  ply1degltdimlem  33782  bnj945  34932  bnj545  35053  bnj548  35055  bnj553  35056  bnj570  35063  bnj929  35094  bnj966  35102  bnj1442  35207  bnj1450  35208  bnj1501  35225  aks6d1c2lem4  42580  aks6d1c2  42583  aks6d1c6lem5  42630  eqresfnbd  42687  idemb  49646