Theorem fnfund 6622

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

Syntax hints:   → wi 4  Fun wfun 6515   Fn wfn 6516

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 209  df-an 400  df-fn 6524

This theorem is referenced by:  ffun  6694  f1fun  6762  imadrhmcl  20846  noseqrdg0  28400  noseqrdgsuc  28401  esplyind  33872  ply1degltdimlem  33919  bnj945  35069  bnj545  35190  bnj548  35192  bnj553  35193  bnj570  35200  bnj929  35231  bnj966  35239  bnj1442  35344  bnj1450  35345  bnj1501  35362  aks6d1c2lem4  42744  aks6d1c2  42747  aks6d1c6lem5  42794  eqresfnbd  42851  idemb  49780