Theorem fnfund 6619

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

Syntax hints:   → wi 4  Fun wfun 6505   Fn wfn 6506

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 6514

This theorem is referenced by:  imadrhmcl  20706  noseqrdg0  28201  noseqrdgsuc  28202  ply1degltdimlem  33618  bnj945  34763  bnj545  34885  bnj548  34887  bnj553  34888  bnj570  34895  bnj929  34926  bnj966  34934  bnj1442  35039  bnj1450  35040  bnj1501  35057  aks6d1c2lem4  42115  aks6d1c2  42118  aks6d1c6lem5  42165  eqresfnbd  42220  idemb  49148