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

Theorem abid 2597
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 2596 . 2 (𝑥 ∈ {𝑥𝜑} ↔ [𝑥 / 𝑥]𝜑)
2 sbid 2099 . 2 ([𝑥 / 𝑥]𝜑𝜑)
31, 2bitri 262 1 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 194  [wsb 1866  wcel 1976  {cab 2595
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-12 2033
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-sb 1867  df-clab 2596
This theorem is referenced by:  abeq2  2718  abeq2d  2720  abbi  2723  abid2f  2776  abeq2f  2777  elabgt  3315  elabgf  3316  ralab2  3337  rexab2  3339  ss2ab  3632  ab0  3904  abn0  3907  sbccsb  3955  sbccsb2  3956  tpid3gOLD  4248  eluniab  4377  elintab  4416  iunab  4496  iinab  4511  zfrep4  4701  sniota  5780  opabiota  6155  eusvobj2  6519  eloprabga  6622  finds2  6963  wfrlem12  7290  en3lplem2  8372  scottexs  8610  scott0s  8611  cp  8614  cardprclem  8665  cfflb  8941  fin23lem29  9023  axdc3lem2  9133  4sqlem12  15446  xkococn  21220  ptcmplem4  21616  ofpreima  28641  qqhval2  29147  esum2dlem  29274  sigaclcu2  29303  bnj1143  29908  bnj1366  29947  bnj906  30047  bnj1256  30130  bnj1259  30131  bnj1311  30139  mclsax  30513  ellines  31222  bj-abeq2  31754  bj-csbsnlem  31873  bj-sspwpwab  32022  topdifinffinlem  32154  finxpreclem6  32192  finxpnom  32197  setindtrs  36393  rababg  36681  compab  37449  tpid3gVD  37882  en3lplem2VD  37884  iunmapsn  38187  ssfiunibd  38247
  Copyright terms: Public domain W3C validator