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

Theorem abid 2430
Description: Simplification of class abstraction notation when the free and bound variables are identical. (Contributed by NM, 26-May-1993.)
Assertion
Ref Expression
abid  |-  ( x  e.  { x  | 
ph }  <->  ph )

Proof of Theorem abid
StepHypRef Expression
1 df-clab 2429 . 2  |-  ( x  e.  { x  | 
ph }  <->  [ x  /  x ] ph )
2 sbid 1982 . 2  |-  ( [ x  /  x ] ph 
<-> 
ph )
31, 2bitri 249 1  |-  ( x  e.  { x  | 
ph }  <->  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   [wsb 1726    e. wcel 1804   {cab 2428
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-12 1840
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-sb 1727  df-clab 2429
This theorem is referenced by:  abeq2  2567  abeq2d  2569  abeq2iOLD  2571  abeq1iOLD  2573  abbi  2574  abid2f  2634  abid2fOLD  2635  elabgt  3229  elabgf  3230  ralab2  3250  rexab2  3252  ss2ab  3553  abn0  3790  sbccsb  3835  sbccsbgOLD  3836  sbccsb2  3837  sbccsb2gOLD  3838  tpid3g  4130  eluniab  4245  elintab  4282  iunab  4361  iinab  4376  zfrep4  4556  sniota  5568  opabiota  5921  eusvobj2  6274  eloprabga  6374  finds2  6713  en3lplem2  8035  scottexs  8308  scott0s  8309  cp  8312  cardprclem  8363  cfflb  8642  fin23lem29  8724  axdc3lem2  8834  4sqlem12  14456  xkococn  20139  ptcmplem4  20533  abeq2f  27376  ofpreima  27485  qqhval2  27941  sigaclcu2  28098  mclsax  28907  wfrlem12  29330  ellines  29778  setindtrs  30943  compab  31304  ssfiunibd  31463  tpid3gVD  33510  en3lplem2VD  33512  bnj1143  33717  bnj1366  33756  bnj906  33856  bnj1256  33939  bnj1259  33940  bnj1311  33948  bj-abeq2  34242  bj-csbsnlem  34353
  Copyright terms: Public domain W3C validator