Theorem fnfun 5325

Description: A function with domain is a function. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
fnfun	⊢ (𝐹 Fn 𝐴 → Fun 𝐹)

Proof of Theorem fnfun

Step	Hyp	Ref	Expression
1		df-fn 5231	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
2	1	simplbi 274	1 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)

Syntax hints:   → wi 4   = wceq 1363  dom cdm 4638  Fun wfun 5222   Fn wfn 5223

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 5231

This theorem is referenced by:  fnrel  5326  funfni  5328  fnco  5336  fnssresb  5340  ffun  5380  f1fun  5436  f1ofun  5475  fnbrfvb  5569  fvelimab  5585  fvun1  5595  elpreima  5648  respreima  5657  fconst3m  5748  fnfvima  5764  fnunirn  5781  f1eqcocnv  5805  fnexALT  6126  tfrlem4  6328  tfrlem5  6329  fndmeng  6824  caseinl  7104  caseinr  7105  cc2lem  7279  shftfn  10847  phimullem  12239  qnnen  12446  prdsex  12736  imasaddvallemg  12754  lidlmex  13664