Theorem fnfun 5418

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 5321	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
2	1	simplbi 274	1 |- ( F Fn A -> Fun F )

Syntax hints:   -> wi 4   = wceq 1395   dom cdm 4719   Fun wfun 5312   Fn wfn 5313

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 5321

This theorem is referenced by:  fnrel  5419  funfni  5423  fnco  5431  fnssresb  5435  ffun  5476  f1fun  5534  f1ofun  5574  fnbrfvb  5672  fvelimab  5690  fvun1  5700  elpreima  5754  respreima  5763  fconst3m  5858  fnfvima  5874  fnunirn  5891  f1eqcocnv  5915  fnexALT  6256  tfrlem4  6459  tfrlem5  6460  fndmeng  6963  caseinl  7258  caseinr  7259  cc2lem  7452  shftfn  11335  phimullem  12747  qnnen  13002  prdsex  13302  prdsval  13306  prdsbaslemss  13307  imasaddvallemg  13348  lidlmex  14439  edgstruct  15864  upgredg  15942