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

Theorem funfn 4874
Description: An equivalence for the function predicate. (Contributed by NM, 13-Aug-2004.)
Assertion
Ref Expression
funfn  Fun  Fn  dom

Proof of Theorem funfn
StepHypRef Expression
1 eqid 2037 . . 3  dom  dom
21biantru 286 . 2  Fun  Fun  dom  dom
3 df-fn 4848 . 2  Fn  dom  Fun  dom  dom
42, 3bitr4i 176 1  Fun  Fn  dom
Colors of variables: wff set class
Syntax hints:   wa 97   wb 98   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  ax-ia2 100  ax-ia3 101  ax-gen 1335  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-cleq 2030  df-fn 4848
This theorem is referenced by:  funssxp  5003  funforn  5056  funbrfvb  5159  funopfvb  5160  ssimaex  5177  fvco  5186  eqfunfv  5213  fvimacnvi  5224  unpreima  5235  respreima  5238  elrnrexdm  5249  elrnrexdmb  5250  ffvresb  5271  resfunexg  5325  funex  5327  elunirn  5348  smores  5848  smores2  5850  tfrlem1  5864
  Copyright terms: Public domain W3C validator