Theorem fnfun 5356

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

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

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 5262

This theorem is referenced by:  fnrel  5357  funfni  5361  fnco  5369  fnssresb  5373  ffun  5413  f1fun  5469  f1ofun  5509  fnbrfvb  5604  fvelimab  5620  fvun1  5630  elpreima  5684  respreima  5693  fconst3m  5784  fnfvima  5800  fnunirn  5817  f1eqcocnv  5841  fnexALT  6177  tfrlem4  6380  tfrlem5  6381  fndmeng  6878  caseinl  7166  caseinr  7167  cc2lem  7349  shftfn  11006  phimullem  12418  qnnen  12673  prdsex  12971  prdsval  12975  prdsbaslemss  12976  imasaddvallemg  13017  lidlmex  14107