Theorem fnfun 5377

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

Syntax hints:   → wi 4   = wceq 1373  dom cdm 4680  Fun wfun 5271   Fn wfn 5272

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 5280

This theorem is referenced by:  fnrel  5378  funfni  5382  fnco  5390  fnssresb  5394  ffun  5435  f1fun  5493  f1ofun  5533  fnbrfvb  5629  fvelimab  5645  fvun1  5655  elpreima  5709  respreima  5718  fconst3m  5813  fnfvima  5829  fnunirn  5846  f1eqcocnv  5870  fnexALT  6206  tfrlem4  6409  tfrlem5  6410  fndmeng  6913  caseinl  7205  caseinr  7206  cc2lem  7391  shftfn  11185  phimullem  12597  qnnen  12852  prdsex  13151  prdsval  13155  prdsbaslemss  13156  imasaddvallemg  13197  lidlmex  14287  edgstruct  15710