Theorem fnfun 5424

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

Syntax hints:   → wi 4   = wceq 1395  dom cdm 4723  Fun wfun 5318   Fn wfn 5319

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 5327

This theorem is referenced by:  fnrel  5425  funfni  5429  fnco  5437  fnssresb  5441  ffun  5482  f1fun  5542  f1ofun  5582  fnbrfvb  5680  fvelimab  5698  fvun1  5708  elpreima  5762  respreima  5771  fncofn  5827  fconst3m  5868  fnfvima  5884  fnunirn  5903  f1eqcocnv  5927  fnexALT  6268  tfrlem4  6474  tfrlem5  6475  fndmeng  6980  caseinl  7284  caseinr  7285  cc2lem  7478  shftfn  11378  phimullem  12790  qnnen  13045  prdsex  13345  prdsval  13349  prdsbaslemss  13350  imasaddvallemg  13391  lidlmex  14482  edgstruct  15908  upgredg  15988