Theorem fnfund 6577

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

Syntax hints:   → wi 4  Fun wfun 6470   Fn wfn 6471

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 6479

This theorem is referenced by:  imadrhmcl  20707  noseqrdg0  28232  noseqrdgsuc  28233  ply1degltdimlem  33627  bnj945  34777  bnj545  34899  bnj548  34901  bnj553  34902  bnj570  34909  bnj929  34940  bnj966  34948  bnj1442  35053  bnj1450  35054  bnj1501  35071  aks6d1c2lem4  42160  aks6d1c2  42163  aks6d1c6lem5  42210  eqresfnbd  42265  idemb  49191