Theorem fnfund 6640

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

This proof depends on syntax axioms:   → wi 4  Fun wfun 6532   Fn wfn 6533

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 6541

This theorem is used by:  ffun  6712  f1fun  6780  imadrhmcl  21054  noseqrdg0  28693  noseqrdgsuc  28694  esplyind  34207  ply1degltdimlem  34254  bnj945  35404  bnj545  35525  bnj548  35527  bnj553  35528  bnj570  35535  bnj929  35566  bnj966  35574  bnj1442  35679  bnj1450  35680  bnj1501  35697  aks6d1c2lem4  43177  aks6d1c2  43180  aks6d1c6lem5  43227  eqresfnbd  43286  idemb  50266