Theorem fnfund 6587

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

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

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 6489

This theorem is referenced by:  imadrhmcl  20701  noseqrdg0  28225  noseqrdgsuc  28226  ply1degltdimlem  33608  bnj945  34759  bnj545  34881  bnj548  34883  bnj553  34884  bnj570  34891  bnj929  34922  bnj966  34930  bnj1442  35035  bnj1450  35036  bnj1501  35053  aks6d1c2lem4  42120  aks6d1c2  42123  aks6d1c6lem5  42170  eqresfnbd  42225  idemb  49164