Theorem fnfun 5421

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

Syntax hints:   → wi 4   = wceq 1395  dom cdm 4720  Fun wfun 5315   Fn wfn 5316

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 5324

This theorem is referenced by:  fnrel  5422  funfni  5426  fnco  5434  fnssresb  5438  ffun  5479  f1fun  5539  f1ofun  5579  fnbrfvb  5677  fvelimab  5695  fvun1  5705  elpreima  5759  respreima  5768  fncofn  5824  fconst3m  5865  fnfvima  5881  fnunirn  5900  f1eqcocnv  5924  fnexALT  6265  tfrlem4  6470  tfrlem5  6471  fndmeng  6976  caseinl  7274  caseinr  7275  cc2lem  7468  shftfn  11356  phimullem  12768  qnnen  13023  prdsex  13323  prdsval  13327  prdsbaslemss  13328  imasaddvallemg  13369  lidlmex  14460  edgstruct  15885  upgredg  15963