Theorem fnfun 5027

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

Syntax hints:   -> wi 4   = wceq 1285   dom cdm 4371   Fun wfun 4926   Fn wfn 4927

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104

This theorem depends on definitions:  df-bi 115  df-fn 4935

This theorem is referenced by:  fnrel  5028  funfni  5030  fnco  5038  fnssresb  5042  ffun  5079  f1fun  5125  f1ofun  5159  fnbrfvb  5246  fvelimab  5261  fvun1  5271  elpreima  5318  respreima  5327  fconst3m  5412  fnfvima  5425  fnunirn  5438  f1eqcocnv  5462  fnexALT  5771  tfrlem4  5962  tfrlem5  5963  fndmeng  6357  shftfn  9850