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

Theorem abid 2423
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 2422 . 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 2421
This theorem is referenced by:  abeq2  2540  abeq2i  2542  abeq1i  2543  abeq2d  2544  abid2f  2596  elabgt  3071  elabgf  3072  ralab2  3091  rexab2  3093  sbccsbg  3271  sbccsb2g  3272  ss2ab  3403  abn0  3638  tpid3g  3911  eluniab  4019  elintab  4053  iunab  4129  iinab  4144  zfrep4  4320  finds2  4865  sniota  5437  eloprabga  6152  opabiota  6530  eusvobj2  6574  en3lplem2  7661  scottexs  7801  scott0s  7802  cp  7805  cardprclem  7856  cfflb  8129  fin23lem29  8211  axdc3lem2  8321  4sqlem12  13314  xkococn  17682  ptcmplem4  18076  abeq2f  23950  ofpreima  24071  qqhval2  24356  sigaclcu2  24493  wfrlem12  25534  ellines  26051  setindtrs  27050  compab  27575  tpid3gVD  28855  en3lplem2VD  28857  bnj1143  29062  bnj1366  29102  bnj906  29202  bnj1256  29285  bnj1259  29286  bnj1311  29294
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 2422
  Copyright terms: Public domain W3C validator