ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fnfun GIF version

Theorem fnfun 5097
Description: A function with domain is a function. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
fnfun (𝐹 Fn 𝐴 → Fun 𝐹)

Proof of Theorem fnfun
StepHypRef Expression
1 df-fn 5005 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
21simplbi 268 1 (𝐹 Fn 𝐴 → Fun 𝐹)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1289  dom cdm 4428  Fun wfun 4996   Fn wfn 4997
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115  df-fn 5005
This theorem is referenced by:  fnrel  5098  funfni  5100  fnco  5108  fnssresb  5112  ffun  5150  f1fun  5203  f1ofun  5239  fnbrfvb  5329  fvelimab  5344  fvun1  5354  elpreima  5402  respreima  5411  fconst3m  5498  fnfvima  5511  fnunirn  5528  f1eqcocnv  5552  fnexALT  5866  tfrlem4  6060  tfrlem5  6061  fndmeng  6507  shftfn  10223  phimullem  11294
  Copyright terms: Public domain W3C validator