Theorem fnfund 6645

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

This proof depends on syntax axioms:   → wi 4  Fun wfun 6537   Fn wfn 6538

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 6546

This theorem is used by:  ffun  6717  f1fun  6785  imadrhmcl  21063  noseqrdg0  28702  noseqrdgsuc  28703  esplyind  34257  ply1degltdimlem  34304  bnj945  35454  bnj545  35575  bnj548  35577  bnj553  35578  bnj570  35585  bnj929  35616  bnj966  35624  bnj1442  35729  bnj1450  35730  bnj1501  35747  aks6d1c2lem4  43314  aks6d1c2  43317  aks6d1c6lem5  43364  eqresfnbd  43423  idemb  50411