Theorem fnfun 5016

Description: A function with domain is a function. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
fnfun	⊢ (𝐹 Fn 𝐴 → Fun 𝐹)

Proof of Theorem fnfun

Step	Hyp	Ref	Expression
1		df-fn 4925	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
2	1	simplbi 268	1 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)

Syntax hints:   → wi 4   = wceq 1284  dom cdm 4363  Fun wfun 4916   Fn wfn 4917

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104

This theorem depends on definitions:  df-bi 115  df-fn 4925

This theorem is referenced by:  fnrel  5017  funfni  5019  fnco  5027  fnssresb  5031  ffun  5068  f1fun  5114  f1ofun  5148  fnbrfvb  5235  fvelimab  5250  fvun1  5260  elpreima  5307  respreima  5316  fconst3m  5401  fnfvima  5414  fnunirn  5427  f1eqcocnv  5451  fnexALT  5760  tfrlem4  5952  tfrlem5  5953  frecsuclem3  6013  fndmeng  6312  frecuzrdgcl  9415  frecuzrdg0  9416  frecuzrdgsuc  9417  shftfn  9712