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

Theorem abid 2431
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 2430 . 2  |-  ( x  e.  { x  | 
ph }  <->  [ x  /  x ] ph )
2 sbid 1940 . 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 1700    e. wcel 1756   {cab 2429
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-sb 1701  df-clab 2430
This theorem is referenced by:  abeq2  2551  abeq2d  2553  abeq2iOLD  2555  abeq1iOLD  2557  abbi  2558  abid2f  2617  abid2fOLD  2618  elabgt  3118  elabgf  3119  ralab2  3139  rexab2  3141  ss2ab  3435  abn0  3671  sbccsb  3716  sbccsbgOLD  3717  sbccsb2  3718  sbccsb2gOLD  3719  tpid3g  4005  eluniab  4117  elintab  4154  iunab  4231  iinab  4246  zfrep4  4426  sniota  5423  opabiota  5769  eusvobj2  6099  eloprabga  6192  finds2  6519  en3lplem2  7836  scottexs  8109  scott0s  8110  cp  8113  cardprclem  8164  cfflb  8443  fin23lem29  8525  axdc3lem2  8635  4sqlem12  14032  xkococn  19248  ptcmplem4  19642  abeq2f  25898  ofpreima  25999  qqhval2  26426  sigaclcu2  26578  wfrlem12  27750  ellines  28198  setindtrs  29393  compab  29716  tpid3gVD  31597  en3lplem2VD  31599  bnj1143  31803  bnj1366  31842  bnj906  31942  bnj1256  32025  bnj1259  32026  bnj1311  32034  bj-abeq2  32313  bj-csbsnlem  32424
  Copyright terms: Public domain W3C validator