Theorem fnfun 5351

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

Syntax hints:   → wi 4   = wceq 1364  dom cdm 4659  Fun wfun 5248   Fn wfn 5249

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

This theorem depends on definitions:  df-bi 117  df-fn 5257

This theorem is referenced by:  fnrel  5352  funfni  5354  fnco  5362  fnssresb  5366  ffun  5406  f1fun  5462  f1ofun  5502  fnbrfvb  5597  fvelimab  5613  fvun1  5623  elpreima  5677  respreima  5686  fconst3m  5777  fnfvima  5793  fnunirn  5810  f1eqcocnv  5834  fnexALT  6163  tfrlem4  6366  tfrlem5  6367  fndmeng  6864  caseinl  7150  caseinr  7151  cc2lem  7326  shftfn  10968  phimullem  12363  qnnen  12588  prdsex  12880  imasaddvallemg  12898  lidlmex  13971