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

Theorem abid 2759
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 2758 . 2 (𝑥 ∈ {𝑥𝜑} ↔ [𝑥 / 𝑥]𝜑)
2 sbid 2270 . 2 ([𝑥 / 𝑥]𝜑𝜑)
31, 2bitri 264 1 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 196  [wsb 2049  wcel 2145  {cab 2757
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-12 2203
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-sb 2050  df-clab 2758
This theorem is referenced by:  abeq2  2881  abeq2d  2883  abbi  2886  abid2f  2940  abeq2f  2941  elabgt  3498  elabgf  3499  ralab2  3523  rexab2  3525  ss2ab  3819  ab0  4098  abn0  4101  sbccsb  4148  sbccsb2  4149  eluniab  4585  elintab  4622  iunab  4700  iinab  4715  zfrep4  4913  sniota  6019  opabiota  6402  eusvobj2  6785  eloprabga  6894  finds2  7241  wfrlem12  7579  en3lplem2  8672  scottexs  8914  scott0s  8915  cp  8918  cardprclem  9005  cfflb  9283  fin23lem29  9365  axdc3lem2  9475  4sqlem12  15863  xkococn  21680  ptcmplem4  22075  ofpreima  29801  qqhval2  30362  esum2dlem  30490  sigaclcu2  30519  bnj1143  31195  bnj1366  31234  bnj906  31334  bnj1256  31417  bnj1259  31418  bnj1311  31426  mclsax  31800  ellines  32592  bj-abeq2  33105  bj-csbsnlem  33223  topdifinffinlem  33528  finxpreclem6  33566  finxpnom  33571  setindtrs  38115  rababg  38402  compab  39168  tpid3gVD  39596  en3lplem2VD  39598  iunmapsn  39924  ssfiunibd  40037  setrec2lem2  42966
  Copyright terms: Public domain W3C validator