Theorem fnfun 5422

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

Syntax hints:   → wi 4   = wceq 1395  dom cdm 4721  Fun wfun 5316   Fn wfn 5317

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 5325

This theorem is referenced by:  fnrel  5423  funfni  5427  fnco  5435  fnssresb  5439  ffun  5480  f1fun  5540  f1ofun  5580  fnbrfvb  5678  fvelimab  5696  fvun1  5706  elpreima  5760  respreima  5769  fncofn  5825  fconst3m  5866  fnfvima  5882  fnunirn  5901  f1eqcocnv  5925  fnexALT  6266  tfrlem4  6472  tfrlem5  6473  fndmeng  6978  caseinl  7279  caseinr  7280  cc2lem  7473  shftfn  11372  phimullem  12784  qnnen  13039  prdsex  13339  prdsval  13343  prdsbaslemss  13344  imasaddvallemg  13385  lidlmex  14476  edgstruct  15901  upgredg  15979