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  5832  fconst3m  5873  fnfvima  5889  fnunirn  5908  f1eqcocnv  5932  fnexALT  6273  tfrlem4  6479  tfrlem5  6480  fndmeng  6985  caseinl  7290  caseinr  7291  cc2lem  7485  shftfn  11402  phimullem  12815  qnnen  13070  prdsex  13370  prdsval  13374  prdsbaslemss  13375  imasaddvallemg  13416  lidlmex  14508  edgstruct  15934  upgredg  16014