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

Theorem eqidd 2038
Description: Class identity law with antecedent. (Contributed by NM, 21-Aug-2008.)
Assertion
Ref Expression
eqidd (φA = A)

Proof of Theorem eqidd
StepHypRef Expression
1 eqid 2037 . 2 A = A
21a1i 9 1 (φA = A)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1242
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
This theorem is referenced by:  cbvraldva  2533  cbvrexdva  2534  nelrdva  2740  opeq2  3541  mpteq1  3832  tfisi  4253  feq23d  4985  fvmptdv2  5203  elrnrexdm  5249  fmptco  5273  ftpg  5290  fliftfun  5379  fliftval  5383  cbvmpt2  5525  eqfnov2  5550  ovmpt2d  5570  ovmpt2dv2  5576  fnofval  5663  ofrval  5664  off  5666  ofres  5667  suppssof1  5670  ofco  5671  caofref  5674  caofrss  5677  caoftrn  5678  rdgivallem  5908  iserd  6068  fzo0to3tp  8825  iseqovex  8879
  Copyright terms: Public domain W3C validator