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

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

Proof of Theorem eqidd
StepHypRef Expression
1 eqid 2083 . 2 𝐴 = 𝐴
21a1i 9 1 (𝜑𝐴 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1285
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1379  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-cleq 2076
This theorem is referenced by:  cbvraldva  2589  cbvrexdva  2590  rspcedeq1vd  2719  rspcedeq2vd  2720  nelrdva  2808  opeq2  3597  mpteq1  3888  tfisi  4365  feq23d  5110  fvmptdv2  5337  elrnrexdm  5383  fmptco  5406  ftpg  5423  fliftfun  5515  fliftval  5519  cbvmpt2  5662  eqfnov2  5687  ovmpt2d  5707  ovmpt2dv2  5713  fnofval  5800  ofrval  5801  off  5803  ofres  5804  suppssof1  5807  ofco  5808  caofref  5811  caofrss  5814  caoftrn  5815  rdgivallem  6078  iserd  6248  1domsn  6465  mapxpen  6494  infrenegsupex  8977  fzo0to3tp  9519  modqsubmod  9678  0tonninf  9734  iseqovex  9748  iseqid  9782  iseqid2  9783  resqrexlemp1rp  10266  resqrexlemfp1  10269  resqrex  10286  climcl  10495  clim2  10496  climuni  10506  climeq  10512  2clim  10514  climshftlemg  10515  climabs0  10520  climcn1  10521  climcn2  10522  climge0  10537  climsqz  10547  climsqz2  10548  climcau  10558  climrecvg1n  10559  climcaucn  10562  serif0  10563  2tp1odd  10664  bezoutlemstep  10766  ialginv  10809  ialgfx  10814  cncongr1  10865  qnumdencoprm  10951  qeqnumdivden  10952  nninfsellemeqinf  11250  exmidsbthrlem  11254
  Copyright terms: Public domain W3C validator