Theorem fnfun 5453

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

Syntax hints:   -> wi 4   = wceq 1398   dom cdm 4749   Fun wfun 5346   Fn wfn 5347

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 5355

This theorem is referenced by:  fnrel  5454  funfni  5458  fnco  5466  fnssresb  5470  ffun  5511  f1fun  5576  f1ofun  5616  fnbrfvb  5715  fvelimab  5733  fvun1  5743  elpreima  5797  respreima  5805  fncofn  5862  fconst3m  5903  fnfvima  5921  fnunirn  5940  f1eqcocnv  5964  fnexALT  6304  suppvalfng  6440  suppvalfn  6441  suppfnss  6457  tfrlem4  6544  tfrlem5  6545  fndmeng  7051  fczfsuppd  7250  caseinl  7382  caseinr  7383  cc2lem  7580  shftfn  11509  phimullem  12922  qnnen  13182  prdsex  13482  prdsval  13486  prdsbaslemss  13487  imasaddvallemg  13528  lidlmex  14623  edgstruct  16059  upgredg  16139