Theorem fnfun 5427

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

Syntax hints:   → wi 4   = wceq 1397  dom cdm 4725  Fun wfun 5320   Fn wfn 5321

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 5329

This theorem is referenced by:  fnrel  5428  funfni  5432  fnco  5440  fnssresb  5444  ffun  5485  f1fun  5545  f1ofun  5585  fnbrfvb  5684  fvelimab  5702  fvun1  5712  elpreima  5766  respreima  5775  fncofn  5832  fconst3m  5873  fnfvima  5889  fnunirn  5908  f1eqcocnv  5932  fnexALT  6273  tfrlem4  6479  tfrlem5  6480  fndmeng  6985  caseinl  7290  caseinr  7291  cc2lem  7485  shftfn  11389  phimullem  12802  qnnen  13057  prdsex  13357  prdsval  13361  prdsbaslemss  13362  imasaddvallemg  13403  lidlmex  14495  edgstruct  15921  upgredg  16001