Theorem fnfun 5335

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

Syntax hints:   -> wi 4   = wceq 1364   dom cdm 4647   Fun wfun 5232   Fn wfn 5233

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

This theorem depends on definitions:  df-bi 117  df-fn 5241

This theorem is referenced by:  fnrel  5336  funfni  5338  fnco  5346  fnssresb  5350  ffun  5390  f1fun  5446  f1ofun  5485  fnbrfvb  5580  fvelimab  5596  fvun1  5606  elpreima  5659  respreima  5668  fconst3m  5759  fnfvima  5775  fnunirn  5792  f1eqcocnv  5816  fnexALT  6140  tfrlem4  6342  tfrlem5  6343  fndmeng  6840  caseinl  7124  caseinr  7125  cc2lem  7300  shftfn  10874  phimullem  12268  qnnen  12493  prdsex  12785  imasaddvallemg  12803  lidlmex  13816