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

Theorem abid 2454
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 2453 . 2  |-  ( x  e.  { x  | 
ph }  <->  [ x  /  x ] ph )
2 sbid 1965 . 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 1711    e. wcel 1767   {cab 2452
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-sb 1712  df-clab 2453
This theorem is referenced by:  abeq2  2591  abeq2d  2593  abeq2iOLD  2595  abeq1iOLD  2597  abbi  2598  abid2f  2658  abid2fOLD  2659  elabgt  3247  elabgf  3248  ralab2  3268  rexab2  3270  ss2ab  3568  abn0  3804  sbccsb  3849  sbccsbgOLD  3850  sbccsb2  3851  sbccsb2gOLD  3852  tpid3g  4142  eluniab  4256  elintab  4293  iunab  4371  iinab  4386  zfrep4  4566  sniota  5576  opabiota  5928  eusvobj2  6275  eloprabga  6371  finds2  6706  en3lplem2  8028  scottexs  8301  scott0s  8302  cp  8305  cardprclem  8356  cfflb  8635  fin23lem29  8717  axdc3lem2  8827  4sqlem12  14329  xkococn  19896  ptcmplem4  20290  abeq2f  27074  ofpreima  27179  qqhval2  27599  sigaclcu2  27760  wfrlem12  28931  ellines  29379  setindtrs  30571  compab  30928  ssfiunibd  31086  tpid3gVD  32722  en3lplem2VD  32724  bnj1143  32928  bnj1366  32967  bnj906  33067  bnj1256  33150  bnj1259  33151  bnj1311  33159  bj-abeq2  33440  bj-csbsnlem  33551
  Copyright terms: Public domain W3C validator