Theorem fnfun 5424

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 5327	. 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 4723   Fun wfun 5318   Fn wfn 5319

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 5327

This theorem is referenced by:  fnrel  5425  funfni  5429  fnco  5437  fnssresb  5441  ffun  5482  f1fun  5542  f1ofun  5582  fnbrfvb  5680  fvelimab  5698  fvun1  5708  elpreima  5762  respreima  5771  fncofn  5827  fconst3m  5868  fnfvima  5884  fnunirn  5903  f1eqcocnv  5927  fnexALT  6268  tfrlem4  6474  tfrlem5  6475  fndmeng  6980  caseinl  7281  caseinr  7282  cc2lem  7475  shftfn  11375  phimullem  12787  qnnen  13042  prdsex  13342  prdsval  13346  prdsbaslemss  13347  imasaddvallemg  13388  lidlmex  14479  edgstruct  15905  upgredg  15983