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

Theorem abid 2790
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 2789 . 2 (𝑥 ∈ {𝑥𝜑} ↔ [𝑥 / 𝑥]𝜑)
2 sbid 2281 . 2 ([𝑥 / 𝑥]𝜑𝜑)
31, 2bitri 266 1 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 197  [wsb 2059  wcel 2155  {cab 2788
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-12 2213
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-sb 2060  df-clab 2789
This theorem is referenced by:  abeq2  2912  abeq2d  2914  abbi  2917  abid2f  2971  abeq2f  2972  elabgt  3538  elabgf  3539  ralab2  3563  rexab2  3565  ss2ab  3861  ab0  4146  abn0  4149  sbccsb  4196  sbccsb2  4197  eluniab  4634  elintab  4673  iunab  4751  iinab  4766  zfrep4  4966  sniota  6085  opabiota  6476  eusvobj2  6861  eloprabga  6971  finds2  7318  wfrlem12  7656  en3lplem2  8749  scottexs  8991  scott0s  8992  cp  8995  cardprclem  9082  cfflb  9360  fin23lem29  9442  axdc3lem2  9552  4sqlem12  15871  xkococn  21671  ptcmplem4  22066  ofpreima  29786  qqhval2  30345  esum2dlem  30473  sigaclcu2  30502  bnj1143  31178  bnj1366  31217  bnj906  31317  bnj1256  31400  bnj1259  31401  bnj1311  31409  mclsax  31783  ellines  32574  bj-abeq2  33081  bj-csbsnlem  33200  topdifinffinlem  33505  finxpreclem6  33543  finxpnom  33548  setindtrs  38087  rababg  38373  compab  39138  tpid3gVD  39565  en3lplem2VD  39567  iunmapsn  39890  ssfiunibd  39998  absnsb  41645  setrec2lem2  43003
  Copyright terms: Public domain W3C validator