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

Theorem fnfun 5024
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 4933 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
21simplbi 263 1 (𝐹 Fn 𝐴 → Fun 𝐹)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1259  dom cdm 4373  Fun wfun 4924   Fn wfn 4925
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103
This theorem depends on definitions:  df-bi 114  df-fn 4933
This theorem is referenced by:  fnrel  5025  funfni  5027  fnco  5035  fnssresb  5039  ffun  5076  f1fun  5122  f1ofun  5156  fnbrfvb  5242  fvelimab  5257  fvun1  5267  elpreima  5314  respreima  5323  fconst3m  5408  fnfvima  5421  fnunirn  5434  f1eqcocnv  5459  fnexALT  5768  tfrlem4  5960  tfrlem5  5961  frecsuclem3  6021  fndmeng  6320  frecuzrdgcl  9363  frecuzrdg0  9364  frecuzrdgsuc  9365  shftfn  9653
  Copyright terms: Public domain W3C validator