Theorem fnfun 5418

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

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  7266  caseinr  7267  cc2lem  7460  shftfn  11343  phimullem  12755  qnnen  13010  prdsex  13310  prdsval  13314  prdsbaslemss  13315  imasaddvallemg  13356  lidlmex  14447  edgstruct  15872  upgredg  15950