Theorem fnfun 5478

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402  dom cdm 4774  Fun wfun 5371   Fn wfn 5372

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-fn 5380

This theorem is used by:  fnrel  5479  funfni  5483  fnco  5491  fnssresb  5495  ffun  5536  f1fun  5601  f1ofun  5641  fnbrfvb  5741  fvelimab  5759  fvun1  5769  elpreima  5828  respreima  5836  fncofn  5893  fconst3m  5934  fnfvima  5953  fnunirn  5973  f1eqcocnv  5997  fnexALT  6340  suppvalfng  6480  suppvalfn  6481  suppfnss  6497  tfrlem4  6584  tfrlem5  6585  fndmeng  7098  fczfsuppd  7297  caseinl  7432  caseinr  7433  cc2lem  7633  shftfn  11604  phimullem  13025  qnnen  13373  imasaddvallemg  13687  prdsex  14223  prdsval  14224  prdsbaslemss  14225  lidlmex  14863  edgstruct  16427  upgredg  16507