Theorem fnfun 5313

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

Syntax hints:   → wi 4   = wceq 1353  dom cdm 4626  Fun wfun 5210   Fn wfn 5211

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 5219

This theorem is referenced by:  fnrel  5314  funfni  5316  fnco  5324  fnssresb  5328  ffun  5368  f1fun  5424  f1ofun  5463  fnbrfvb  5556  fvelimab  5572  fvun1  5582  elpreima  5635  respreima  5644  fconst3m  5735  fnfvima  5751  fnunirn  5767  f1eqcocnv  5791  fnexALT  6111  tfrlem4  6313  tfrlem5  6314  fndmeng  6809  caseinl  7089  caseinr  7090  cc2lem  7264  shftfn  10832  phimullem  12224  qnnen  12431  prdsex  12717  imasaddvallemg  12735