Theorem fnfun 5293

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

Syntax hints:   -> wi 4   = wceq 1348   dom cdm 4609   Fun wfun 5190   Fn wfn 5191

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 5199

This theorem is referenced by:  fnrel  5294  funfni  5296  fnco  5304  fnssresb  5308  ffun  5348  f1fun  5404  f1ofun  5442  fnbrfvb  5535  fvelimab  5550  fvun1  5560  elpreima  5613  respreima  5622  fconst3m  5713  fnfvima  5728  fnunirn  5744  f1eqcocnv  5768  fnexALT  6088  tfrlem4  6290  tfrlem5  6291  fndmeng  6786  caseinl  7066  caseinr  7067  cc2lem  7221  shftfn  10781  phimullem  12172  qnnen  12379