Theorem fnfun 5215

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

Syntax hints:   -> wi 4   = wceq 1331   dom cdm 4534   Fun wfun 5112   Fn wfn 5113

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

This theorem depends on definitions:  df-bi 116  df-fn 5121

This theorem is referenced by:  fnrel  5216  funfni  5218  fnco  5226  fnssresb  5230  ffun  5270  f1fun  5326  f1ofun  5362  fnbrfvb  5455  fvelimab  5470  fvun1  5480  elpreima  5532  respreima  5541  fconst3m  5632  fnfvima  5645  fnunirn  5661  f1eqcocnv  5685  fnexALT  6004  tfrlem4  6203  tfrlem5  6204  fndmeng  6697  caseinl  6969  caseinr  6970  shftfn  10589  phimullem  11890  qnnen  11933