Theorem fnfun 5285

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

Syntax hints:   → wi 4   = wceq 1343  dom cdm 4604  Fun wfun 5182   Fn wfn 5183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-fn 5191

This theorem is referenced by:  fnrel  5286  funfni  5288  fnco  5296  fnssresb  5300  ffun  5340  f1fun  5396  f1ofun  5434  fnbrfvb  5527  fvelimab  5542  fvun1  5552  elpreima  5604  respreima  5613  fconst3m  5704  fnfvima  5719  fnunirn  5735  f1eqcocnv  5759  fnexALT  6079  tfrlem4  6281  tfrlem5  6282  fndmeng  6776  caseinl  7056  caseinr  7057  cc2lem  7207  shftfn  10766  phimullem  12157  qnnen  12364