MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  abid Unicode version

Theorem abid 2444
Description: Simplification of class abstraction notation when the free and bound variables are identical. (Contributed by NM, 26-May-1993.)
Assertion
Ref Expression
abid

Proof of Theorem abid
StepHypRef Expression
1 df-clab 2443 . 2
2 sbid 1996 . 2
31, 2bitri 249 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  [wsb 1739  e.wcel 1818  {cab 2442
This theorem is referenced by:  abeq2  2581  abeq2d  2583  abeq2iOLD  2585  abeq1iOLD  2587  abbi  2588  abid2f  2648  abid2fOLD  2649  elabgt  3243  elabgf  3244  ralab2  3264  rexab2  3266  ss2ab  3567  abn0  3804  sbccsb  3849  sbccsbgOLD  3850  sbccsb2  3851  sbccsb2gOLD  3852  tpid3g  4145  eluniab  4260  elintab  4297  iunab  4376  iinab  4391  zfrep4  4571  sniota  5583  opabiota  5936  eusvobj2  6289  eloprabga  6389  finds2  6728  en3lplem2  8053  scottexs  8326  scott0s  8327  cp  8330  cardprclem  8381  cfflb  8660  fin23lem29  8742  axdc3lem2  8852  4sqlem12  14474  xkococn  20161  ptcmplem4  20555  abeq2f  27398  ofpreima  27507  qqhval2  27963  sigaclcu2  28120  mclsax  28929  wfrlem12  29354  ellines  29802  setindtrs  30967  compab  31350  ssfiunibd  31509  tpid3gVD  33642  en3lplem2VD  33644  bnj1143  33849  bnj1366  33888  bnj906  33988  bnj1256  34071  bnj1259  34072  bnj1311  34080  bj-abeq2  34359  bj-csbsnlem  34470
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-sb 1740  df-clab 2443
  Copyright terms: Public domain W3C validator