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

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

Proof of Theorem eqidd
StepHypRef Expression
1 eqid 2056 . 2  |-  A  =  A
21a1i 9 1  |-  ( ph  ->  A  =  A )
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  2769  opeq2  3578  mpteq1  3869  tfisi  4338  feq23d  5070  fvmptdv2  5288  elrnrexdm  5334  fmptco  5358  ftpg  5375  fliftfun  5464  fliftval  5468  cbvmpt2  5611  eqfnov2  5636  ovmpt2d  5656  ovmpt2dv2  5662  fnofval  5749  ofrval  5750  off  5752  ofres  5753  suppssof1  5756  ofco  5757  caofref  5760  caofrss  5763  caoftrn  5764  rdgivallem  5999  iserd  6163  fzo0to3tp  9177  modqsubmod  9332  iseqovex  9383  iseqid  9411  resqrexlemp1rp  9833  resqrexlemfp1  9836  resqrex  9853  climcl  10034  clim2  10035  climuni  10045  climeq  10051  2clim  10053  climshftlemg  10054  climabs0  10059  climcn1  10060  climcn2  10061  climge0  10076  climsqz  10086  climsqz2  10087  climcau  10097  climrecvg1n  10098  climcaucn  10101  serif0  10102  2tp1odd  10196  ialginv  10269  ialgfx  10274
  Copyright terms: Public domain W3C validator