Theorem fnfun 5418

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

Syntax hints:   -> wi 4   = wceq 1395   dom cdm 4719   Fun wfun 5312   Fn wfn 5313

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 5321

This theorem is referenced by:  fnrel  5419  funfni  5423  fnco  5431  fnssresb  5435  ffun  5476  f1fun  5536  f1ofun  5576  fnbrfvb  5674  fvelimab  5692  fvun1  5702  elpreima  5756  respreima  5765  fncofn  5821  fconst3m  5862  fnfvima  5878  fnunirn  5897  f1eqcocnv  5921  fnexALT  6262  tfrlem4  6465  tfrlem5  6466  fndmeng  6971  caseinl  7269  caseinr  7270  cc2lem  7463  shftfn  11351  phimullem  12763  qnnen  13018  prdsex  13318  prdsval  13322  prdsbaslemss  13323  imasaddvallemg  13364  lidlmex  14455  edgstruct  15880  upgredg  15958