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

Theorem abid 2740
 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 2739 . 2 (𝑥 ∈ {𝑥𝜑} ↔ [𝑥 / 𝑥]𝜑)
2 sbid 2253 . 2 ([𝑥 / 𝑥]𝜑𝜑)
31, 2bitri 264 1 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196  [wsb 2038   ∈ wcel 2131  {cab 2738 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-12 2188 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1846  df-sb 2039  df-clab 2739 This theorem is referenced by:  abeq2  2862  abeq2d  2864  abbi  2867  abid2f  2921  abeq2f  2922  elabgt  3479  elabgf  3480  ralab2  3504  rexab2  3506  ss2ab  3803  ab0  4086  abn0  4089  sbccsb  4139  sbccsb2  4140  eluniab  4591  elintab  4631  iunab  4710  iinab  4725  zfrep4  4923  sniota  6031  opabiota  6415  eusvobj2  6798  eloprabga  6904  finds2  7251  wfrlem12  7587  en3lplem2  8673  scottexs  8915  scott0s  8916  cp  8919  cardprclem  8987  cfflb  9265  fin23lem29  9347  axdc3lem2  9457  4sqlem12  15854  xkococn  21657  ptcmplem4  22052  ofpreima  29766  qqhval2  30327  esum2dlem  30455  sigaclcu2  30484  bnj1143  31160  bnj1366  31199  bnj906  31299  bnj1256  31382  bnj1259  31383  bnj1311  31391  mclsax  31765  ellines  32557  bj-abeq2  33071  bj-csbsnlem  33196  topdifinffinlem  33498  finxpreclem6  33536  finxpnom  33541  setindtrs  38086  rababg  38373  compab  39139  tpid3gVD  39568  en3lplem2VD  39570  iunmapsn  39900  ssfiunibd  40014  setrec2lem2  42943
 Copyright terms: Public domain W3C validator