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

Theorem eqidd 2178
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 2177 . 2  |-  A  =  A
21a1i 9 1  |-  ( ph  ->  A  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1353
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1449  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170
This theorem is referenced by:  cbvraldva  2712  cbvrexdva  2713  rspcedeq1vd  2850  rspcedeq2vd  2851  nelrdva  2944  opeq2  3777  mpteq1  4084  tfisi  4582  feq23d  5356  fvmptdv2  5600  elrnrexdm  5650  fmptco  5677  cofmpt  5680  ftpg  5695  fliftfun  5790  fliftval  5794  cbvmpo  5947  fconstmpo  5963  eqfnov2  5975  ovmpod  5995  ovmpodv2  6001  ofvalg  6085  ofrval  6086  off  6088  ofres  6090  suppssof1  6093  ofco  6094  caofref  6097  caofrss  6100  caoftrn  6101  rdgivallem  6375  iserd  6554  ixpsnf1o  6729  1domsn  6812  mapxpen  6841  infnninf  7115  ctssexmid  7141  nninfdcinf  7162  nninfwlporlemd  7163  nninfwlporlem  7164  nninfwlpoimlemginf  7167  infrenegsupex  9570  fz0to4untppr  10097  fzo0to3tp  10192  modqsubmod  10355  0tonninf  10412  iseqovex  10429  seqvalcd  10432  seq3f1olemqsumkj  10471  seq3id  10481  seq3id2  10482  resqrexlemp1rp  10986  resqrexlemfp1  10989  resqrex  11006  infxrnegsupex  11242  climcl  11261  clim2  11262  climuni  11272  climeq  11278  2clim  11280  climshftlemg  11281  climabs0  11286  climcn1  11287  climcn2  11288  climge0  11304  climsqz  11314  climsqz2  11315  climcau  11326  climrecvg1n  11327  climcaucn  11330  serf0  11331  isumz  11368  fisumss  11371  fsumsplitsn  11389  fsumsplitsnun  11398  isumclim3  11402  isummulc2  11405  fsum2dlemstep  11413  fsumconst  11433  fsumabs  11444  fsumparts  11449  iserabs  11454  fsumiun  11456  isumshft  11469  cvgratnnlemseq  11505  mertenslemub  11513  mertenslemi1  11514  mertenslem2  11515  prod1dc  11565  fprodssdc  11569  fprodunsn  11583  fprodcl2lem  11584  fprodconst  11599  fprod2dlemstep  11601  fprodsplitsn  11612  eftlcl  11667  reeftlcl  11668  eftlub  11669  efsep  11670  effsumlt  11671  eirraplem  11755  2tp1odd  11859  bezoutlemstep  11968  alginv  12017  algfx  12022  cncongr1  12073  qnumdencoprm  12163  qeqnumdivden  12164  ctiunctal  12412  unct  12413  nninfdclemcl  12419  nninfdclemf  12420  nninfdclemp1  12421  nninfdc  12424  ressressg  12503  issgrp  12688  sgrp1  12695  ismndd  12717  mndprop  12721  insubm  12749  grpprop  12771  grpsubfvalg  12795  grpsubpropdg  12850  mulgfvalg  12861  mulgpropdg  12900  ablprop  12914  subcmnd  12943  issrg  12961  srgidmlem  12974  isring  12996  ringass  13012  ringidmlem  13018  ringabl  13028  ringprop  13032  isringd  13033  ring1  13049  opprring  13061  opprringbg  13062  mulgass3  13066  dvdsrcld  13078  dvdsrex  13079  dvdsrcl2  13080  dvdsrid  13081  dvdsrtr  13082  dvdsrneg  13084  dvdsr01  13085  1unit  13088  unitcld  13089  opprunitd  13091  crngunit  13092  unitmulcl  13094  unitgrpbasd  13096  unitgrp  13097  unitabl  13098  unitgrpid  13099  unitsubm  13100  unitlinv  13107  unitrinv  13108  unitnegcl  13111  epttop  13223  lmss  13379  txlm  13412  lmcn2  13413  cnmpt2c  13423  txswaphmeolem  13453  blfvalps  13518  bdxmet  13634  fsumcncntop  13689  cncfmptc  13715  cncfmpt1f  13717  cdivcncfap  13720  negfcncf  13722  dvidlemap  13793  dvcnp2cntop  13796  dvaddxxbr  13798  dvmulxxbr  13799  dviaddf  13802  dvexp  13808  dvmptaddx  13814  dvmptmulx  13815  dvef  13821  sincn  13823  coscn  13824  lgsdir2lem5  14066  2sqlem8  14092  nninfsellemeqinf  14388  nninffeq  14392  exmidsbthrlem  14393  cvgcmp2nlemabs  14403
  Copyright terms: Public domain W3C validator