Theorem fnfun 5473

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

Syntax hints:   -> wi 4   = wceq 1402   dom cdm 4769   Fun wfun 5366   Fn wfn 5367

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 5375

This theorem is referenced by:  fnrel  5474  funfni  5478  fnco  5486  fnssresb  5490  ffun  5531  f1fun  5596  f1ofun  5636  fnbrfvb  5735  fvelimab  5753  fvun1  5763  elpreima  5819  respreima  5827  fncofn  5884  fconst3m  5925  fnfvima  5943  fnunirn  5963  f1eqcocnv  5987  fnexALT  6330  suppvalfng  6470  suppvalfn  6471  suppfnss  6487  tfrlem4  6574  tfrlem5  6575  fndmeng  7088  fczfsuppd  7287  caseinl  7421  caseinr  7422  cc2lem  7622  shftfn  11567  phimullem  12981  qnnen  13300  imasaddvallemg  13613  prdsex  14149  prdsval  14150  prdsbaslemss  14151  lidlmex  14784  edgstruct  16219  upgredg  16299