Theorem fnfun 5452

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

Syntax hints:   → wi 4   = wceq 1398  dom cdm 4748  Fun wfun 5345   Fn wfn 5346

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 5354

This theorem is referenced by:  fnrel  5453  funfni  5457  fnco  5465  fnssresb  5469  ffun  5510  f1fun  5575  f1ofun  5615  fnbrfvb  5714  fvelimab  5732  fvun1  5742  elpreima  5796  respreima  5804  fncofn  5861  fconst3m  5902  fnfvima  5920  fnunirn  5939  f1eqcocnv  5963  fnexALT  6303  suppvalfng  6439  suppvalfn  6440  suppfnss  6456  tfrlem4  6543  tfrlem5  6544  fndmeng  7050  fczfsuppd  7249  caseinl  7381  caseinr  7382  cc2lem  7579  shftfn  11505  phimullem  12918  qnnen  13174  prdsex  13474  prdsval  13478  prdsbaslemss  13479  imasaddvallemg  13520  lidlmex  14615  edgstruct  16051  upgredg  16131