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

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

Proof of Theorem abid
StepHypRef Expression
1 df-clab 2283 . 2  |-  ( x  e.  { x  | 
ph }  <->  [ x  /  x ] ph )
2 sbid 1875 . 2  |-  ( [ x  /  x ] ph 
<-> 
ph )
31, 2bitri 240 1  |-  ( x  e.  { x  | 
ph }  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   [wsb 1638    e. wcel 1696   {cab 2282
This theorem is referenced by:  abeq2  2401  abeq2i  2403  abeq1i  2404  abeq2d  2405  abid2f  2457  elabgt  2924  elabgf  2925  ralab2  2943  rexab2  2945  sbccsbg  3122  sbccsb2g  3123  ss2ab  3254  abn0  3486  tpid3g  3754  eluniab  3855  elintab  3889  iunab  3964  iinab  3979  zfrep4  4155  finds2  4700  sniota  5262  eloprabga  5950  opabiota  6309  eusvobj2  6353  en3lplem2  7433  scottexs  7573  scott0s  7574  cp  7577  cardprclem  7628  cfflb  7901  fin23lem29  7983  axdc3lem2  8093  4sqlem12  13019  xkococn  17370  ptcmplem4  17765  ballotth  23112  abeq2f  23145  rabid2f  23151  ssiun3  23172  ofrn2  23222  sigaclcuni  23494  sigaclcu2  23496  ellines  24847  dominc  25383  rninc  25384  setindtrs  27221  compab  27747  tpid3gVD  28934  en3lplem2VD  28936  bnj1143  29138  bnj1366  29178  bnj906  29278  bnj1256  29361  bnj1259  29362  bnj1311  29370
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-sb 1639  df-clab 2283
  Copyright terms: Public domain W3C validator