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 6508   Fn wfn 6509

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 207  df-an 396  df-fn 6517

This theorem is referenced by:  imadrhmcl  20713  noseqrdg0  28208  noseqrdgsuc  28209  ply1degltdimlem  33625  bnj945  34770  bnj545  34892  bnj548  34894  bnj553  34895  bnj570  34902  bnj929  34933  bnj966  34941  bnj1442  35046  bnj1450  35047  bnj1501  35064  aks6d1c2lem4  42122  aks6d1c2  42125  aks6d1c6lem5  42172  eqresfnbd  42227  idemb  49152