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

Theorem abid 2800
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 2797 . 2 (𝑥 ∈ {𝑥𝜑} ↔ [𝑥 / 𝑥]𝜑)
2 sbid 2247 . 2 ([𝑥 / 𝑥]𝜑𝜑)
31, 2bitri 276 1 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 207  [wsb 2060  wcel 2105  {cab 2796
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-12 2167
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061  df-clab 2797
This theorem is referenced by:  abeq2  2942  abeq2d  2944  abbiOLD  2952  abid2f  3009  abeq2f  3010  abeq2fOLD  3011  elabgt  3660  elabgf  3661  elabg  3663  ralab2  3685  ralab2OLD  3686  rexab2  3688  rexab2OLD  3689  ss2ab  4036  ab0  4330  abn0  4333  sbccsb  4382  sbccsb2  4383  eluniab  4841  elintab  4878  iunab  4966  iinab  4981  zfrep4  5191  rnep  5790  sniota  6339  opabiota  6739  eusvobj2  7138  eloprabga  7250  finds2  7599  wfrlem12  7955  en3lplem2  9064  scottexs  9304  scott0s  9305  cp  9308  cardprclem  9396  cfflb  9669  fin23lem29  9751  axdc3lem2  9861  4sqlem12  16280  xkococn  22196  ptcmplem4  22591  ofpreima  30338  qqhval2  31122  esum2dlem  31250  sigaclcu2  31278  bnj1143  31961  bnj1366  32000  bnj906  32101  bnj1256  32184  bnj1259  32185  bnj1311  32193  mclsax  32713  frrlem10  33029  ellines  33510  bj-csbsnlem  34117  bj-reabeq  34236  topdifinffinlem  34510  rdgssun  34541  finxpreclem6  34559  finxpnom  34564  ralssiun  34570  setindtrs  39500  rababg  39811  scottabf  40453  compab  40651  tpid3gVD  41053  en3lplem2VD  41055  iunmapsn  41356  ssfiunibd  41452  absnsb  43139  symgsubmefmndALT  43996  setrec2lem2  44725
  Copyright terms: Public domain W3C validator