Theorem fnfun 5481

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   dom cdm 4776   Fun wfun 5374   Fn wfn 5375

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-fn 5383

This theorem is used by:  fnrel  5482  funfni  5486  fnco  5494  fnssresb  5498  ffun  5539  f1fun  5604  f1ofun  5644  fnbrfvb  5744  fvelimab  5762  fvun1  5772  elpreima  5831  respreima  5839  fncofn  5896  fconst3m  5937  fnfvima  5956  fnunirn  5976  f1eqcocnv  6000  fnexALT  6344  suppvalfng  6484  suppvalfn  6485  suppfnss  6501  tfrlem4  6589  tfrlem5  6590  fndmeng  7104  fczfsuppd  7304  caseinl  7437  caseinr  7438  cc2lem  7638  shftfn  11610  phimullem  13031  qnnen  13379  imasaddvallemg  13694  prdsex  14278  prdsval  14279  prdsbaslemss  14280  lidlmex  14920  edgstruct  16527  upgredg  16607