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

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

Proof of Theorem eqidd
StepHypRef Expression
1 eqid 2139 . 2 𝐴 = 𝐴
21a1i 9 1 (𝜑𝐴 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1331
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 1425  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-cleq 2132
This theorem is referenced by:  cbvraldva  2663  cbvrexdva  2664  rspcedeq1vd  2798  rspcedeq2vd  2799  nelrdva  2891  opeq2  3706  mpteq1  4012  tfisi  4501  feq23d  5268  fvmptdv2  5510  elrnrexdm  5559  fmptco  5586  cofmpt  5589  ftpg  5604  fliftfun  5697  fliftval  5701  cbvmpo  5850  fconstmpo  5866  eqfnov2  5878  ovmpod  5898  ovmpodv2  5904  ofvalg  5991  ofrval  5992  off  5994  ofres  5996  suppssof1  5999  ofco  6000  caofref  6003  caofrss  6006  caoftrn  6007  rdgivallem  6278  iserd  6455  ixpsnf1o  6630  1domsn  6713  mapxpen  6742  ctssexmid  7024  infrenegsupex  9401  fzo0to3tp  10008  modqsubmod  10167  0tonninf  10224  iseqovex  10241  seqvalcd  10244  seq3f1olemqsumkj  10283  seq3id  10293  seq3id2  10294  resqrexlemp1rp  10790  resqrexlemfp1  10793  resqrex  10810  infxrnegsupex  11044  climcl  11063  clim2  11064  climuni  11074  climeq  11080  2clim  11082  climshftlemg  11083  climabs0  11088  climcn1  11089  climcn2  11090  climge0  11106  climsqz  11116  climsqz2  11117  climcau  11128  climrecvg1n  11129  climcaucn  11132  serf0  11133  isumz  11170  fisumss  11173  fsumsplitsn  11191  fsumsplitsnun  11200  isumclim3  11204  isummulc2  11207  fsum2dlemstep  11215  fsumconst  11235  fsumabs  11246  fsumparts  11251  iserabs  11256  fsumiun  11258  isumshft  11271  cvgratnnlemseq  11307  mertenslemub  11315  mertenslemi1  11316  mertenslem2  11317  eftlcl  11406  reeftlcl  11407  eftlub  11408  efsep  11409  effsumlt  11410  eirraplem  11494  2tp1odd  11592  bezoutlemstep  11696  alginv  11739  algfx  11744  cncongr1  11795  qnumdencoprm  11882  qeqnumdivden  11883  ctiunctal  11965  unct  11966  epttop  12273  lmss  12429  txlm  12462  lmcn2  12463  cnmpt2c  12473  txswaphmeolem  12503  blfvalps  12568  bdxmet  12684  fsumcncntop  12739  cncfmptc  12765  cncfmpt1f  12767  cdivcncfap  12770  negfcncf  12772  dvidlemap  12843  dvcnp2cntop  12846  dvaddxxbr  12848  dvmulxxbr  12849  dviaddf  12852  dvexp  12858  dvmptaddx  12864  dvmptmulx  12865  dvef  12871  sincn  12873  coscn  12874  nninfsellemeqinf  13298  nninffeq  13302  exmidsbthrlem  13303  cvgcmp2nlemabs  13313
  Copyright terms: Public domain W3C validator