Theorem fnfun 5315

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

Syntax hints:   → wi 4   = wceq 1353  dom cdm 4628  Fun wfun 5212   Fn wfn 5213

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 5221

This theorem is referenced by:  fnrel  5316  funfni  5318  fnco  5326  fnssresb  5330  ffun  5370  f1fun  5426  f1ofun  5465  fnbrfvb  5558  fvelimab  5574  fvun1  5584  elpreima  5637  respreima  5646  fconst3m  5737  fnfvima  5753  fnunirn  5770  f1eqcocnv  5794  fnexALT  6114  tfrlem4  6316  tfrlem5  6317  fndmeng  6812  caseinl  7092  caseinr  7093  cc2lem  7267  shftfn  10835  phimullem  12227  qnnen  12434  prdsex  12723  imasaddvallemg  12741