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

Theorem abid 2450
Description: Simplification of class abstraction notation when the free and bound variables are identical. (Contributed by NM, 26-May-1993.)
Assertion
Ref Expression
abid  |-  ( x  e.  { x  | 
ph }  <->  ph )

Proof of Theorem abid
StepHypRef Expression
1 df-clab 2449 . 2  |-  ( x  e.  { x  | 
ph }  <->  [ x  /  x ] ph )
2 sbid 2097 . 2  |-  ( [ x  /  x ] ph 
<-> 
ph )
31, 2bitri 257 1  |-  ( x  e.  { x  | 
ph }  <->  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189   [wsb 1808    e. wcel 1898   {cab 2448
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-12 1944
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675  df-sb 1809  df-clab 2449
This theorem is referenced by:  abeq2  2571  abeq2d  2573  abbi  2576  abid2f  2629  abeq2f  2630  elabgt  3194  elabgf  3195  ralab2  3215  rexab2  3217  ss2ab  3509  abn0  3763  sbccsb  3805  sbccsb2  3806  tpid3g  4100  eluniab  4223  elintab  4259  iunab  4338  iinab  4353  zfrep4  4537  sniota  5592  opabiota  5951  eusvobj2  6308  eloprabga  6410  finds2  6748  wfrlem12  7073  en3lplem2  8146  scottexs  8384  scott0s  8385  cp  8388  cardprclem  8439  cfflb  8715  fin23lem29  8797  axdc3lem2  8907  4sqlem12  14949  xkococn  20724  ptcmplem4  21119  ofpreima  28317  qqhval2  28835  esum2dlem  28962  sigaclcu2  28991  bnj1143  29651  bnj1366  29690  bnj906  29790  bnj1256  29873  bnj1259  29874  bnj1311  29882  mclsax  30256  ellines  30968  bj-abeq2  31433  bj-csbsnlem  31550  topdifinffinlem  31795  finxpreclem6  31833  finxpnom  31838  setindtrs  35925  rababg  36224  compab  36838  tpid3gVD  37278  en3lplem2VD  37280  ssfiunibd  37565
  Copyright terms: Public domain W3C validator