Theorem fnfun 5371

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

Syntax hints:   -> wi 4   = wceq 1373   dom cdm 4675   Fun wfun 5265   Fn wfn 5266

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 5274

This theorem is referenced by:  fnrel  5372  funfni  5376  fnco  5384  fnssresb  5388  ffun  5428  f1fun  5484  f1ofun  5524  fnbrfvb  5619  fvelimab  5635  fvun1  5645  elpreima  5699  respreima  5708  fconst3m  5803  fnfvima  5819  fnunirn  5836  f1eqcocnv  5860  fnexALT  6196  tfrlem4  6399  tfrlem5  6400  fndmeng  6902  caseinl  7193  caseinr  7194  cc2lem  7378  shftfn  11135  phimullem  12547  qnnen  12802  prdsex  13101  prdsval  13105  prdsbaslemss  13106  imasaddvallemg  13147  lidlmex  14237  edgstruct  15656