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  7431  caseinr  7432  cc2lem  7632  shftfn  11591  phimullem  13005  qnnen  13324  imasaddvallemg  13638  prdsex  14174  prdsval  14175  prdsbaslemss  14176  lidlmex  14814  edgstruct  16317  upgredg  16397