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

Theorem abid 2424
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 2423 . 2  |-  ( x  e.  { x  | 
ph }  <->  [ x  /  x ] ph )
2 sbid 1947 . 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 1658    e. wcel 1725   {cab 2422
This theorem is referenced by:  abeq2  2541  abeq2i  2543  abeq1i  2544  abeq2d  2545  abid2f  2597  elabgt  3079  elabgf  3080  ralab2  3099  rexab2  3101  sbccsbg  3279  sbccsb2g  3280  ss2ab  3411  abn0  3646  tpid3g  3919  eluniab  4027  elintab  4061  iunab  4137  iinab  4152  zfrep4  4328  finds2  4873  sniota  5445  eloprabga  6160  opabiota  6538  eusvobj2  6582  en3lplem2  7671  scottexs  7811  scott0s  7812  cp  7815  cardprclem  7866  cfflb  8139  fin23lem29  8221  axdc3lem2  8331  4sqlem12  13324  xkococn  17692  ptcmplem4  18086  abeq2f  23960  ofpreima  24081  qqhval2  24366  sigaclcu2  24503  wfrlem12  25549  ellines  26086  setindtrs  27096  compab  27620  tpid3gVD  28954  en3lplem2VD  28956  bnj1143  29161  bnj1366  29201  bnj906  29301  bnj1256  29384  bnj1259  29385  bnj1311  29393
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-sb 1659  df-clab 2423
  Copyright terms: Public domain W3C validator