Theorem fnfun 5434

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

Syntax hints:   → wi 4   = wceq 1398  dom cdm 4731  Fun wfun 5327   Fn wfn 5328

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 5336

This theorem is referenced by:  fnrel  5435  funfni  5439  fnco  5447  fnssresb  5451  ffun  5492  f1fun  5554  f1ofun  5594  fnbrfvb  5693  fvelimab  5711  fvun1  5721  elpreima  5775  respreima  5783  fncofn  5840  fconst3m  5881  fnfvima  5899  fnunirn  5918  f1eqcocnv  5942  fnexALT  6282  suppvalfng  6418  suppvalfn  6419  suppfnss  6435  tfrlem4  6522  tfrlem5  6523  fndmeng  7028  caseinl  7333  caseinr  7334  cc2lem  7528  shftfn  11445  phimullem  12858  qnnen  13113  prdsex  13413  prdsval  13417  prdsbaslemss  13418  imasaddvallemg  13459  lidlmex  14551  edgstruct  15985  upgredg  16065