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

Theorem abid 2598
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 2597 . 2 (𝑥 ∈ {𝑥𝜑} ↔ [𝑥 / 𝑥]𝜑)
2 sbid 2100 . 2 ([𝑥 / 𝑥]𝜑𝜑)
31, 2bitri 263 1 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 195  [wsb 1867  wcel 1977  {cab 2596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034
This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-sb 1868  df-clab 2597
This theorem is referenced by:  abeq2  2719  abeq2d  2721  abbi  2724  abid2f  2777  abeq2f  2778  elabgt  3316  elabgf  3317  ralab2  3338  rexab2  3340  ss2ab  3633  ab0  3905  abn0  3908  sbccsb  3956  sbccsb2  3957  tpid3gOLD  4249  eluniab  4383  elintab  4422  iunab  4502  iinab  4517  zfrep4  4707  sniota  5795  opabiota  6171  eusvobj2  6542  eloprabga  6645  finds2  6986  wfrlem12  7313  en3lplem2  8395  scottexs  8633  scott0s  8634  cp  8637  cardprclem  8688  cfflb  8964  fin23lem29  9046  axdc3lem2  9156  4sqlem12  15498  xkococn  21273  ptcmplem4  21669  ofpreima  28848  qqhval2  29354  esum2dlem  29481  sigaclcu2  29510  bnj1143  30115  bnj1366  30154  bnj906  30254  bnj1256  30337  bnj1259  30338  bnj1311  30346  mclsax  30720  ellines  31429  bj-abeq2  31961  bj-csbsnlem  32090  bj-sspwpwab  32239  topdifinffinlem  32371  finxpreclem6  32409  finxpnom  32414  setindtrs  36610  rababg  36898  compab  37666  tpid3gVD  38099  en3lplem2VD  38101  iunmapsn  38404  ssfiunibd  38464  setrec2lem2  42240
  Copyright terms: Public domain W3C validator