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

Theorem abid 2377
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 2376 . 2  |-  ( x  e.  { x  | 
ph }  <->  [ x  /  x ] ph )
2 sbid 1936 . 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 1717   {cab 2375
This theorem is referenced by:  abeq2  2494  abeq2i  2496  abeq1i  2497  abeq2d  2498  abid2f  2550  elabgt  3024  elabgf  3025  ralab2  3044  rexab2  3046  sbccsbg  3224  sbccsb2g  3225  ss2ab  3356  abn0  3591  tpid3g  3864  eluniab  3971  elintab  4005  iunab  4080  iinab  4095  zfrep4  4271  finds2  4815  sniota  5387  eloprabga  6101  opabiota  6476  eusvobj2  6520  en3lplem2  7606  scottexs  7746  scott0s  7747  cp  7750  cardprclem  7801  cfflb  8074  fin23lem29  8156  axdc3lem2  8266  4sqlem12  13253  xkococn  17615  ptcmplem4  18009  abeq2f  23806  qqhval2  24167  sigaclcu2  24301  ellines  25802  setindtrs  26789  compab  27314  tpid3gVD  28297  en3lplem2VD  28299  bnj1143  28501  bnj1366  28541  bnj906  28641  bnj1256  28724  bnj1259  28725  bnj1311  28733
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 1661  ax-8 1682  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-sb 1656  df-clab 2376
  Copyright terms: Public domain W3C validator