Theorem fnfun 5390

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

Syntax hints:   -> wi 4   = wceq 1373   dom cdm 4693   Fun wfun 5284   Fn wfn 5285

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 5293

This theorem is referenced by:  fnrel  5391  funfni  5395  fnco  5403  fnssresb  5407  ffun  5448  f1fun  5506  f1ofun  5546  fnbrfvb  5642  fvelimab  5658  fvun1  5668  elpreima  5722  respreima  5731  fconst3m  5826  fnfvima  5842  fnunirn  5859  f1eqcocnv  5883  fnexALT  6219  tfrlem4  6422  tfrlem5  6423  fndmeng  6926  caseinl  7219  caseinr  7220  cc2lem  7413  shftfn  11250  phimullem  12662  qnnen  12917  prdsex  13216  prdsval  13220  prdsbaslemss  13221  imasaddvallemg  13262  lidlmex  14352  edgstruct  15775  upgredg  15848