Theorem fnfun 5111

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

Syntax hints:   -> wi 4   = wceq 1289   dom cdm 4438   Fun wfun 5009   Fn wfn 5010

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 5018

This theorem is referenced by:  fnrel  5112  funfni  5114  fnco  5122  fnssresb  5126  ffun  5164  f1fun  5219  f1ofun  5255  fnbrfvb  5345  fvelimab  5360  fvun1  5370  elpreima  5418  respreima  5427  fconst3m  5516  fnfvima  5529  fnunirn  5546  f1eqcocnv  5570  fnexALT  5884  tfrlem4  6078  tfrlem5  6079  fndmeng  6525  shftfn  10254  phimullem  11475