Theorem fnfund 6634

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

This proof depends on syntax axioms:   → wi 4  Fun wfun 6527   Fn wfn 6528

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 6536

This theorem is used by:  ffun  6706  f1fun  6774  imadrhmcl  20964  noseqrdg0  28573  noseqrdgsuc  28574  esplyind  34086  ply1degltdimlem  34133  bnj945  35284  bnj545  35405  bnj548  35407  bnj553  35408  bnj570  35415  bnj929  35446  bnj966  35454  bnj1442  35559  bnj1450  35560  bnj1501  35577  aks6d1c2lem4  42994  aks6d1c2  42997  aks6d1c6lem5  43044  eqresfnbd  43103  idemb  50086