Theorem fnfund 6670

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

This proof depends on syntax axioms:   → wi 4  Fun wfun 6560   Fn wfn 6561

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fn 6569

This theorem is used by:  ffun  6742  f1fun  6810  imadrhmcl  21105  noseqrdg0  28750  noseqrdgsuc  28751  esplyind  34318  ply1degltdimlem  34365  bnj945  35515  bnj545  35636  bnj548  35638  bnj553  35639  bnj570  35646  bnj929  35677  bnj966  35685  bnj1442  35790  bnj1450  35791  bnj1501  35808  aks6d1c2lem4  43443  aks6d1c2  43446  aks6d1c6lem5  43493  eqresfnbd  43553  idemb  50606