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

Theorem eqidd 2141
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 2140 . 2  |-  A  =  A
21a1i 9 1  |-  ( ph  ->  A  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1332
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1426  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-cleq 2133
This theorem is referenced by:  cbvraldva  2664  cbvrexdva  2665  rspcedeq1vd  2799  rspcedeq2vd  2800  nelrdva  2892  opeq2  3710  mpteq1  4016  tfisi  4505  feq23d  5272  fvmptdv2  5514  elrnrexdm  5563  fmptco  5590  cofmpt  5593  ftpg  5608  fliftfun  5701  fliftval  5705  cbvmpo  5854  fconstmpo  5870  eqfnov2  5882  ovmpod  5902  ovmpodv2  5908  ofvalg  5995  ofrval  5996  off  5998  ofres  6000  suppssof1  6003  ofco  6004  caofref  6007  caofrss  6010  caoftrn  6011  rdgivallem  6282  iserd  6459  ixpsnf1o  6634  1domsn  6717  mapxpen  6746  ctssexmid  7028  infrenegsupex  9412  fzo0to3tp  10023  modqsubmod  10182  0tonninf  10239  iseqovex  10256  seqvalcd  10259  seq3f1olemqsumkj  10298  seq3id  10308  seq3id2  10309  resqrexlemp1rp  10806  resqrexlemfp1  10809  resqrex  10826  infxrnegsupex  11060  climcl  11079  clim2  11080  climuni  11090  climeq  11096  2clim  11098  climshftlemg  11099  climabs0  11104  climcn1  11105  climcn2  11106  climge0  11122  climsqz  11132  climsqz2  11133  climcau  11144  climrecvg1n  11145  climcaucn  11148  serf0  11149  isumz  11186  fisumss  11189  fsumsplitsn  11207  fsumsplitsnun  11216  isumclim3  11220  isummulc2  11223  fsum2dlemstep  11231  fsumconst  11251  fsumabs  11262  fsumparts  11267  iserabs  11272  fsumiun  11274  isumshft  11287  cvgratnnlemseq  11323  mertenslemub  11331  mertenslemi1  11332  mertenslem2  11333  eftlcl  11422  reeftlcl  11423  eftlub  11424  efsep  11425  effsumlt  11426  eirraplem  11510  2tp1odd  11608  bezoutlemstep  11712  alginv  11755  algfx  11760  cncongr1  11811  qnumdencoprm  11898  qeqnumdivden  11899  ctiunctal  11981  unct  11982  epttop  12289  lmss  12445  txlm  12478  lmcn2  12479  cnmpt2c  12489  txswaphmeolem  12519  blfvalps  12584  bdxmet  12700  fsumcncntop  12755  cncfmptc  12781  cncfmpt1f  12783  cdivcncfap  12786  negfcncf  12788  dvidlemap  12859  dvcnp2cntop  12862  dvaddxxbr  12864  dvmulxxbr  12865  dviaddf  12868  dvexp  12874  dvmptaddx  12880  dvmptmulx  12881  dvef  12887  sincn  12889  coscn  12890  nninfsellemeqinf  13370  nninffeq  13374  exmidsbthrlem  13375  cvgcmp2nlemabs  13385
  Copyright terms: Public domain W3C validator