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

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

Proof of Theorem fnfun
StepHypRef Expression
1 df-fn 4848 . 2 (𝐹 Fn A ↔ (Fun 𝐹 dom 𝐹 = A))
21simplbi 259 1 (𝐹 Fn A → Fun 𝐹)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1242  dom cdm 4288  Fun wfun 4839   Fn wfn 4840
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99
This theorem depends on definitions:  df-bi 110  df-fn 4848
This theorem is referenced by:  fnrel  4940  funfni  4942  fnco  4950  fnssresb  4954  ffun  4991  f1fun  5037  f1ofun  5071  fnbrfvb  5157  fvelimab  5172  fvun1  5182  elpreima  5229  respreima  5238  fconst3m  5323  fnfvima  5336  fnunirn  5349  f1eqcocnv  5374  fnexALT  5682  tfrlem4  5870  tfrlem5  5871  frecsuclem3  5929  fndmeng  6225  frecuzrdgcl  8860  frecuzrdg0  8861  frecuzrdgsuc  8862
  Copyright terms: Public domain W3C validator