Theorem fnfun 5220

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

Syntax hints:   → wi 4   = wceq 1331  dom cdm 4539  Fun wfun 5117   Fn wfn 5118

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 5126

This theorem is referenced by:  fnrel  5221  funfni  5223  fnco  5231  fnssresb  5235  ffun  5275  f1fun  5331  f1ofun  5369  fnbrfvb  5462  fvelimab  5477  fvun1  5487  elpreima  5539  respreima  5548  fconst3m  5639  fnfvima  5652  fnunirn  5668  f1eqcocnv  5692  fnexALT  6011  tfrlem4  6210  tfrlem5  6211  fndmeng  6704  caseinl  6976  caseinr  6977  shftfn  10596  phimullem  11901  qnnen  11944