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  7431  caseinr  7432  cc2lem  7632  shftfn  11589  phimullem  13003  qnnen  13322  imasaddvallemg  13636  prdsex  14172  prdsval  14173  prdsbaslemss  14174  lidlmex  14812  edgstruct  16305  upgredg  16385