Theorem fnfun 5228

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

Syntax hints:   -> wi 4   = wceq 1332   dom cdm 4547   Fun wfun 5125   Fn wfn 5126

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

This theorem depends on definitions:  df-bi 116  df-fn 5134

This theorem is referenced by:  fnrel  5229  funfni  5231  fnco  5239  fnssresb  5243  ffun  5283  f1fun  5339  f1ofun  5377  fnbrfvb  5470  fvelimab  5485  fvun1  5495  elpreima  5547  respreima  5556  fconst3m  5647  fnfvima  5660  fnunirn  5676  f1eqcocnv  5700  fnexALT  6019  tfrlem4  6218  tfrlem5  6219  fndmeng  6712  caseinl  6984  caseinr  6985  cc2lem  7098  shftfn  10628  phimullem  11937  qnnen  11980