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

Theorem abid 2409
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 2408 . 2  |-  ( x  e.  { x  | 
ph }  <->  [ x  /  x ] ph )
2 sbid 2050 . 2  |-  ( [ x  /  x ] ph 
<-> 
ph )
31, 2bitri 252 1  |-  ( x  e.  { x  | 
ph }  <->  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187   [wsb 1786    e. wcel 1868   {cab 2407
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-12 1905
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-sb 1787  df-clab 2408
This theorem is referenced by:  abeq2  2546  abeq2d  2548  abeq2iOLD  2550  abeq1iOLD  2552  abbi  2553  abid2f  2613  abid2fOLD  2614  abeq2f  2615  elabgt  3215  elabgf  3216  ralab2  3236  rexab2  3238  ss2ab  3529  abn0  3781  sbccsb  3821  sbccsb2  3822  tpid3g  4112  eluniab  4227  elintab  4263  iunab  4342  iinab  4357  zfrep4  4541  sniota  5589  opabiota  5941  eusvobj2  6295  eloprabga  6394  finds2  6732  wfrlem12  7052  en3lplem2  8123  scottexs  8360  scott0s  8361  cp  8364  cardprclem  8415  cfflb  8690  fin23lem29  8772  axdc3lem2  8882  4sqlem12  14888  xkococn  20662  ptcmplem4  21057  ofpreima  28258  qqhval2  28782  esum2dlem  28909  sigaclcu2  28938  bnj1143  29598  bnj1366  29637  bnj906  29737  bnj1256  29820  bnj1259  29821  bnj1311  29829  mclsax  30203  ellines  30912  bj-abeq2  31346  bj-csbsnlem  31462  topdifinffinlem  31691  setindtrs  35800  compab  36652  tpid3gVD  37099  en3lplem2VD  37101  ssfiunibd  37369
  Copyright terms: Public domain W3C validator