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

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

Proof of Theorem funfn
StepHypRef Expression
1 eqid 2037 . . 3 dom A = dom A
21biantru 286 . 2 (Fun A ↔ (Fun A dom A = dom A))
3 df-fn 4848 . 2 (A Fn dom A ↔ (Fun A dom A = dom A))
42, 3bitr4i 176 1 (Fun AA Fn dom A)
 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