Theorem fnfun 5260

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

Syntax hints:   → wi 4   = wceq 1332  dom cdm 4579  Fun wfun 5157   Fn wfn 5158

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 5166

This theorem is referenced by:  fnrel  5261  funfni  5263  fnco  5271  fnssresb  5275  ffun  5315  f1fun  5371  f1ofun  5409  fnbrfvb  5502  fvelimab  5517  fvun1  5527  elpreima  5579  respreima  5588  fconst3m  5679  fnfvima  5692  fnunirn  5708  f1eqcocnv  5732  fnexALT  6051  tfrlem4  6250  tfrlem5  6251  fndmeng  6744  caseinl  7021  caseinr  7022  cc2lem  7165  shftfn  10701  phimullem  12068  qnnen  12111