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

Theorem abid 2389
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 2388 . 2  |-  ( x  e.  { x  | 
ph }  <->  [ x  /  x ] ph )
2 sbid 2023 . 2  |-  ( [ x  /  x ] ph 
<-> 
ph )
31, 2bitri 249 1  |-  ( x  e.  { x  | 
ph }  <->  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   [wsb 1763    e. wcel 1842   {cab 2387
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-12 1878
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1634  df-sb 1764  df-clab 2388
This theorem is referenced by:  abeq2  2526  abeq2d  2528  abeq2iOLD  2530  abeq1iOLD  2532  abbi  2533  abid2f  2593  abid2fOLD  2594  abeq2f  2595  elabgt  3192  elabgf  3193  ralab2  3213  rexab2  3215  ss2ab  3506  abn0  3757  sbccsb  3797  sbccsb2  3798  tpid3g  4086  eluniab  4201  elintab  4237  iunab  4316  iinab  4331  zfrep4  4514  sniota  5559  opabiota  5911  eusvobj2  6270  eloprabga  6369  finds2  6711  wfrlem12  7031  en3lplem2  8064  scottexs  8336  scott0s  8337  cp  8340  cardprclem  8391  cfflb  8670  fin23lem29  8752  axdc3lem2  8862  4sqlem12  14681  xkococn  20451  ptcmplem4  20845  ofpreima  27936  qqhval2  28401  esum2dlem  28525  sigaclcu2  28554  bnj1143  29163  bnj1366  29202  bnj906  29302  bnj1256  29385  bnj1259  29386  bnj1311  29394  mclsax  29768  ellines  30477  bj-abeq2  30910  bj-csbsnlem  31021  topdifinffinlem  31251  setindtrs  35309  compab  36178  tpid3gVD  36652  en3lplem2VD  36654  ssfiunibd  36858
  Copyright terms: Public domain W3C validator