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

Theorem abid 2396
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 2395 . 2  |-  ( x  e.  { x  | 
ph }  <->  [ x  /  x ] ph )
2 sbid 1943 . 2  |-  ( [ x  /  x ] ph 
<-> 
ph )
31, 2bitri 241 1  |-  ( x  e.  { x  | 
ph }  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 177   [wsb 1655    e. wcel 1721   {cab 2394
This theorem is referenced by:  abeq2  2513  abeq2i  2515  abeq1i  2516  abeq2d  2517  abid2f  2569  elabgt  3043  elabgf  3044  ralab2  3063  rexab2  3065  sbccsbg  3243  sbccsb2g  3244  ss2ab  3375  abn0  3610  tpid3g  3883  eluniab  3991  elintab  4025  iunab  4101  iinab  4116  zfrep4  4292  finds2  4836  sniota  5408  eloprabga  6123  opabiota  6501  eusvobj2  6545  en3lplem2  7631  scottexs  7771  scott0s  7772  cp  7775  cardprclem  7826  cfflb  8099  fin23lem29  8181  axdc3lem2  8291  4sqlem12  13283  xkococn  17649  ptcmplem4  18043  abeq2f  23917  ofpreima  24038  qqhval2  24323  sigaclcu2  24460  ellines  25994  setindtrs  26990  compab  27515  tpid3gVD  28667  en3lplem2VD  28669  bnj1143  28871  bnj1366  28911  bnj906  29011  bnj1256  29094  bnj1259  29095  bnj1311  29103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-sb 1656  df-clab 2395
  Copyright terms: Public domain W3C validator