Theorem fnfund 6665

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

Syntax hints:   → wi 4  Fun wfun 6552   Fn wfn 6553

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 206  df-an 395  df-fn 6561

This theorem is referenced by:  imadrhmcl  20798  noseqrdg0  28304  noseqrdgsuc  28305  ply1degltdimlem  33548  bnj945  34656  bnj545  34778  bnj548  34780  bnj553  34781  bnj570  34788  bnj929  34819  bnj966  34827  bnj1442  34932  bnj1450  34933  bnj1501  34950  aks6d1c2lem4  41873  aks6d1c2  41876  aks6d1c6lem5  41923  eqresfnbd  42012