Theorem fnfun 5414

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

Syntax hints:   → wi 4   = wceq 1395  dom cdm 4716  Fun wfun 5308   Fn wfn 5309

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 5317

This theorem is referenced by:  fnrel  5415  funfni  5419  fnco  5427  fnssresb  5431  ffun  5472  f1fun  5530  f1ofun  5570  fnbrfvb  5666  fvelimab  5683  fvun1  5693  elpreima  5747  respreima  5756  fconst3m  5851  fnfvima  5867  fnunirn  5884  f1eqcocnv  5908  fnexALT  6246  tfrlem4  6449  tfrlem5  6450  fndmeng  6953  caseinl  7246  caseinr  7247  cc2lem  7440  shftfn  11321  phimullem  12733  qnnen  12988  prdsex  13288  prdsval  13292  prdsbaslemss  13293  imasaddvallemg  13334  lidlmex  14424  edgstruct  15849  upgredg  15927