Theorem fnfun 5295

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

Syntax hints:   → wi 4   = wceq 1348  dom cdm 4611  Fun wfun 5192   Fn wfn 5193

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 5201

This theorem is referenced by:  fnrel  5296  funfni  5298  fnco  5306  fnssresb  5310  ffun  5350  f1fun  5406  f1ofun  5444  fnbrfvb  5537  fvelimab  5552  fvun1  5562  elpreima  5615  respreima  5624  fconst3m  5715  fnfvima  5730  fnunirn  5746  f1eqcocnv  5770  fnexALT  6090  tfrlem4  6292  tfrlem5  6293  fndmeng  6788  caseinl  7068  caseinr  7069  cc2lem  7228  shftfn  10788  phimullem  12179  qnnen  12386