Theorem fnfun 5434

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 5336	. 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 4731   Fun wfun 5327   Fn wfn 5328

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 5336

This theorem is referenced by:  fnrel  5435  funfni  5439  fnco  5447  fnssresb  5451  ffun  5492  f1fun  5554  f1ofun  5594  fnbrfvb  5693  fvelimab  5711  fvun1  5721  elpreima  5775  respreima  5783  fncofn  5840  fconst3m  5881  fnfvima  5899  fnunirn  5918  f1eqcocnv  5942  fnexALT  6282  suppvalfng  6418  suppvalfn  6419  suppfnss  6435  tfrlem4  6522  tfrlem5  6523  fndmeng  7028  fczfsuppd  7222  caseinl  7350  caseinr  7351  cc2lem  7545  shftfn  11464  phimullem  12877  qnnen  13132  prdsex  13432  prdsval  13436  prdsbaslemss  13437  imasaddvallemg  13478  lidlmex  14571  edgstruct  16005  upgredg  16085