Theorem fnfun 5355

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

Syntax hints:   → wi 4   = wceq 1364  dom cdm 4663  Fun wfun 5252   Fn wfn 5253

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 5261

This theorem is referenced by:  fnrel  5356  funfni  5358  fnco  5366  fnssresb  5370  ffun  5410  f1fun  5466  f1ofun  5506  fnbrfvb  5601  fvelimab  5617  fvun1  5627  elpreima  5681  respreima  5690  fconst3m  5781  fnfvima  5797  fnunirn  5814  f1eqcocnv  5838  fnexALT  6168  tfrlem4  6371  tfrlem5  6372  fndmeng  6869  caseinl  7157  caseinr  7158  cc2lem  7333  shftfn  10989  phimullem  12393  qnnen  12648  prdsex  12940  imasaddvallemg  12958  lidlmex  14031