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

Theorem abid 2780
 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 2777 . 2 (𝑥 ∈ {𝑥𝜑} ↔ [𝑥 / 𝑥]𝜑)
2 sbid 2254 . 2 ([𝑥 / 𝑥]𝜑𝜑)
31, 2bitri 278 1 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209  [wsb 2069   ∈ wcel 2111  {cab 2776 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2175 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777 This theorem is referenced by:  abeq2  2922  abeq2d  2924  abbiOLD  2930  abid2f  2984  abeq2f  2985  elabgt  3609  elabgf  3610  elabg  3614  ralab2  3636  ralab2OLD  3637  rexab2  3639  rexab2OLD  3640  ss2ab  3987  ab0  4287  abn0  4290  sbccsb  4341  sbccsb2  4342  eluniab  4815  elintab  4849  iunab  4938  iinab  4953  zfrep4  5164  rnep  5761  sniota  6315  opabiota  6721  eusvobj2  7128  eloprabga  7240  finds2  7593  wfrlem12  7951  en3lplem2  9062  scottexs  9302  scott0s  9303  cp  9306  cardprclem  9394  cfflb  9672  fin23lem29  9754  axdc3lem2  9864  4sqlem12  16284  xkococn  22272  ptcmplem4  22667  ofpreima  30435  qqhval2  31345  esum2dlem  31473  sigaclcu2  31501  bnj1143  32184  bnj1366  32223  bnj906  32324  bnj1256  32409  bnj1259  32410  bnj1311  32418  mclsax  32941  frrlem10  33257  ellines  33738  bj-csbsnlem  34360  bj-reabeq  34479  topdifinffinlem  34780  rdgssun  34811  finxpreclem6  34829  finxpnom  34834  ralssiun  34840  setindtrs  39981  rababg  40288  scottabf  40963  compab  41161  tpid3gVD  41563  en3lplem2VD  41565  iunmapsn  41861  ssfiunibd  41956  absnsb  43634  setrec2lem2  45238
 Copyright terms: Public domain W3C validator