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  6588  tfrlem5  6589  fndmeng  7102  fczfsuppd  7302  caseinl  7437  caseinr  7438  cc2lem  7638  shftfn  11611  phimullem  13032  qnnen  13380  imasaddvallemg  13695  prdsex  14279  prdsval  14280  prdsbaslemss  14281  lidlmex  14921  edgstruct  16510  upgredg  16590