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

Theorem eqidd 2019
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 2018 . 2 A = A
21a1i 9 1 (φA = A)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1226
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 1314  ax-ext 2000
This theorem depends on definitions:  df-bi 110  df-cleq 2011
This theorem is referenced by:  cbvraldva  2513  cbvrexdva  2514  nelrdva  2719  opeq2  3520  mpteq1  3811  tfisi  4233  feq23d  4964  fvmptdv2  5181  elrnrexdm  5227  fmptco  5251  ftpg  5268  fliftfun  5357  fliftval  5361  cbvmpt2  5502  eqfnov2  5527  ovmpt2d  5547  ovmpt2dv2  5553  fnofval  5640  ofrval  5641  off  5643  ofres  5644  suppssof1  5647  ofco  5648  caofref  5651  caofrss  5654  caoftrn  5655  rdgivallem  5884  iserd  6039
  Copyright terms: Public domain W3C validator