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

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

Proof of Theorem eqidd
StepHypRef Expression
1 eqid 2056 . 2 𝐴 = 𝐴
21a1i 9 1 (𝜑𝐴 = 𝐴)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1259 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-gen 1354  ax-ext 2038 This theorem depends on definitions:  df-bi 114  df-cleq 2049 This theorem is referenced by:  cbvraldva  2556  cbvrexdva  2557  rspcedeq1vd  2681  rspcedeq2vd  2682  nelrdva  2768  opeq2  3577  mpteq1  3868  tfisi  4337  feq23d  5069  fvmptdv2  5287  elrnrexdm  5333  fmptco  5357  ftpg  5374  fliftfun  5463  fliftval  5467  cbvmpt2  5610  eqfnov2  5635  ovmpt2d  5655  ovmpt2dv2  5661  fnofval  5748  ofrval  5749  off  5751  ofres  5752  suppssof1  5755  ofco  5756  caofref  5759  caofrss  5762  caoftrn  5763  rdgivallem  5998  iserd  6162  fzo0to3tp  9176  modqsubmod  9331  iseqovex  9382  iseqid  9410  resqrexlemp1rp  9832  resqrexlemfp1  9835  resqrex  9852  climcl  10033  clim2  10034  climuni  10044  climeq  10050  2clim  10052  climshftlemg  10053  climabs0  10058  climcn1  10059  climcn2  10060  climge0  10075  climsqz  10085  climsqz2  10086  climcau  10096  climrecvg1n  10097  climcaucn  10100  serif0  10101  2tp1odd  10195  ialginv  10248  ialgfx  10253
 Copyright terms: Public domain W3C validator