Theorem fnfun 4996

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 4905	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
2	1	simplbi 259	1 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)

Syntax hints:   → wi 4   = wceq 1243  dom cdm 4345  Fun wfun 4896   Fn wfn 4897

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

This theorem depends on definitions:  df-bi 110  df-fn 4905

This theorem is referenced by:  fnrel  4997  funfni  4999  fnco  5007  fnssresb  5011  ffun  5048  f1fun  5094  f1ofun  5128  fnbrfvb  5214  fvelimab  5229  fvun1  5239  elpreima  5286  respreima  5295  fconst3m  5380  fnfvima  5393  fnunirn  5406  f1eqcocnv  5431  fnexALT  5740  tfrlem4  5929  tfrlem5  5930  frecsuclem3  5990  fndmeng  6289  frecuzrdgcl  9199  frecuzrdg0  9200  frecuzrdgsuc  9201  shftfn  9425