Theorem fnfun 5427

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

Syntax hints:   -> wi 4   = wceq 1397   dom cdm 4725   Fun wfun 5320   Fn wfn 5321

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 5329

This theorem is referenced by:  fnrel  5428  funfni  5432  fnco  5440  fnssresb  5444  ffun  5485  f1fun  5545  f1ofun  5585  fnbrfvb  5684  fvelimab  5702  fvun1  5712  elpreima  5766  respreima  5775  fncofn  5831  fconst3m  5872  fnfvima  5888  fnunirn  5907  f1eqcocnv  5931  fnexALT  6272  tfrlem4  6478  tfrlem5  6479  fndmeng  6984  caseinl  7289  caseinr  7290  cc2lem  7484  shftfn  11384  phimullem  12796  qnnen  13051  prdsex  13351  prdsval  13355  prdsbaslemss  13356  imasaddvallemg  13397  lidlmex  14488  edgstruct  15914  upgredg  15994