Theorem fnfun 5476

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 5378	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
2	1	simplbi 274	1 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)

Syntax hints:   → wi 4   = wceq 1402  dom cdm 4772  Fun wfun 5369   Fn wfn 5370

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 5378

This theorem is referenced by:  fnrel  5477  funfni  5481  fnco  5489  fnssresb  5493  ffun  5534  f1fun  5599  f1ofun  5639  fnbrfvb  5738  fvelimab  5756  fvun1  5766  elpreima  5822  respreima  5830  fncofn  5887  fconst3m  5928  fnfvima  5947  fnunirn  5967  f1eqcocnv  5991  fnexALT  6334  suppvalfng  6474  suppvalfn  6475  suppfnss  6491  tfrlem4  6578  tfrlem5  6579  fndmeng  7092  fczfsuppd  7291  caseinl  7425  caseinr  7426  cc2lem  7626  shftfn  11572  phimullem  12986  qnnen  13305  imasaddvallemg  13619  prdsex  14155  prdsval  14156  prdsbaslemss  14157  lidlmex  14795  edgstruct  16288  upgredg  16368