Theorem fnfun 5458

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

Syntax hints:   → wi 4   = wceq 1398  dom cdm 4754  Fun wfun 5351   Fn wfn 5352

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 5360

This theorem is referenced by:  fnrel  5459  funfni  5463  fnco  5471  fnssresb  5475  ffun  5516  f1fun  5581  f1ofun  5621  fnbrfvb  5720  fvelimab  5738  fvun1  5748  elpreima  5802  respreima  5810  fncofn  5867  fconst3m  5908  fnfvima  5926  fnunirn  5946  f1eqcocnv  5970  fnexALT  6313  suppvalfng  6453  suppvalfn  6454  suppfnss  6470  tfrlem4  6557  tfrlem5  6558  fndmeng  7064  fczfsuppd  7263  caseinl  7395  caseinr  7396  cc2lem  7596  shftfn  11534  phimullem  12947  qnnen  13266  prdsex  13566  prdsval  13570  prdsbaslemss  13571  imasaddvallemg  13612  lidlmex  14735  edgstruct  16171  upgredg  16251