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

Theorem abid 2354
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 2353 . 2  |-  ( x  e.  { x  | 
ph }  <->  [ x  /  x ] ph )
2 sbid 1934 . 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 1653    e. wcel 1715   {cab 2352
This theorem is referenced by:  abeq2  2471  abeq2i  2473  abeq1i  2474  abeq2d  2475  abid2f  2527  elabgt  2996  elabgf  2997  ralab2  3016  rexab2  3018  sbccsbg  3195  sbccsb2g  3196  ss2ab  3327  abn0  3561  tpid3g  3834  eluniab  3941  elintab  3975  iunab  4050  iinab  4065  zfrep4  4241  finds2  4787  sniota  5349  eloprabga  6060  opabiota  6435  eusvobj2  6479  en3lplem2  7564  scottexs  7704  scott0s  7705  cp  7708  cardprclem  7759  cfflb  8032  fin23lem29  8114  axdc3lem2  8224  4sqlem12  13211  xkococn  17571  ptcmplem4  17962  abeq2f  23348  rabid2f  23355  ssiun3  23407  ofrn2  23456  cnextf  23702  qqhval2  23838  sigaclcuni  23966  sigaclcu2  23968  ballotth  24243  ellines  25517  setindtrs  26624  compab  27150  tpid3gVD  28382  en3lplem2VD  28384  bnj1143  28586  bnj1366  28626  bnj906  28726  bnj1256  28809  bnj1259  28810  bnj1311  28818
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-11 1751
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1547  df-sb 1654  df-clab 2353
  Copyright terms: Public domain W3C validator