Theorem fnfun 5372

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 5275	. 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 4676   Fun wfun 5266   Fn wfn 5267

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 5275

This theorem is referenced by:  fnrel  5373  funfni  5377  fnco  5385  fnssresb  5389  ffun  5430  f1fun  5486  f1ofun  5526  fnbrfvb  5621  fvelimab  5637  fvun1  5647  elpreima  5701  respreima  5710  fconst3m  5805  fnfvima  5821  fnunirn  5838  f1eqcocnv  5862  fnexALT  6198  tfrlem4  6401  tfrlem5  6402  fndmeng  6904  caseinl  7195  caseinr  7196  cc2lem  7380  shftfn  11168  phimullem  12580  qnnen  12835  prdsex  13134  prdsval  13138  prdsbaslemss  13139  imasaddvallemg  13180  lidlmex  14270  edgstruct  15691