Theorem fnfun 5478

Description: A function with domain is a function. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
fnfun	|- ( F Fn A -> Fun F )

Proof of Theorem fnfun

Step	Hyp	Ref	Expression
1		df-fn 5380	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
2	1	simplbi 274	1 |- ( F Fn A -> Fun F )

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  11605  phimullem  13026  qnnen  13374  imasaddvallemg  13689  prdsex  14256  prdsval  14257  prdsbaslemss  14258  lidlmex  14896  edgstruct  16471  upgredg  16551