Theorem fnfun 5352

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

Syntax hints:   -> wi 4   = wceq 1364   dom cdm 4660   Fun wfun 5249   Fn wfn 5250

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 5258

This theorem is referenced by:  fnrel  5353  funfni  5355  fnco  5363  fnssresb  5367  ffun  5407  f1fun  5463  f1ofun  5503  fnbrfvb  5598  fvelimab  5614  fvun1  5624  elpreima  5678  respreima  5687  fconst3m  5778  fnfvima  5794  fnunirn  5811  f1eqcocnv  5835  fnexALT  6165  tfrlem4  6368  tfrlem5  6369  fndmeng  6866  caseinl  7152  caseinr  7153  cc2lem  7328  shftfn  10971  phimullem  12366  qnnen  12591  prdsex  12883  imasaddvallemg  12901  lidlmex  13974