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

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

Proof of Theorem eqidd
StepHypRef Expression
1 eqid 2085 . 2 𝐴 = 𝐴
21a1i 9 1 (𝜑𝐴 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1287
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 1381  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078
This theorem is referenced by:  cbvraldva  2592  cbvrexdva  2593  rspcedeq1vd  2722  rspcedeq2vd  2723  nelrdva  2811  opeq2  3606  mpteq1  3897  tfisi  4375  feq23d  5122  fvmptdv2  5355  elrnrexdm  5401  fmptco  5427  ftpg  5444  fliftfun  5536  fliftval  5540  cbvmpt2  5684  eqfnov2  5709  ovmpt2d  5729  ovmpt2dv2  5735  fnofval  5822  ofrval  5823  off  5825  ofres  5826  suppssof1  5829  ofco  5830  caofref  5833  caofrss  5836  caoftrn  5837  rdgivallem  6100  iserd  6270  1domsn  6487  mapxpen  6516  infrenegsupex  9014  fzo0to3tp  9558  modqsubmod  9717  0tonninf  9773  iseqovex  9787  iseqf1olemqsumkj  9832  iseqid  9843  iseqid2  9844  resqrexlemp1rp  10335  resqrexlemfp1  10338  resqrex  10355  climcl  10565  clim2  10566  climuni  10576  climeq  10582  2clim  10584  climshftlemg  10585  climabs0  10590  climcn1  10591  climcn2  10592  climge0  10607  climsqz  10617  climsqz2  10618  climcau  10628  climrecvg1n  10629  climcaucn  10632  serif0  10633  isumz  10669  fisumss  10672  2tp1odd  10766  bezoutlemstep  10868  ialginv  10911  ialgfx  10916  cncongr1  10967  qnumdencoprm  11053  qeqnumdivden  11054  nninfsellemeqinf  11353  exmidsbthrlem  11357
  Copyright terms: Public domain W3C validator