Theorem fnfund 6644

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

Syntax hints:   → wi 4  Fun wfun 6530   Fn wfn 6531

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 6539

This theorem is referenced by:  imadrhmcl  20762  noseqrdg0  28258  noseqrdgsuc  28259  ply1degltdimlem  33667  bnj945  34809  bnj545  34931  bnj548  34933  bnj553  34934  bnj570  34941  bnj929  34972  bnj966  34980  bnj1442  35085  bnj1450  35086  bnj1501  35103  aks6d1c2lem4  42145  aks6d1c2  42148  aks6d1c6lem5  42195  eqresfnbd  42250