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

Theorem abid 2271
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 2270 . 2  |-  ( x  e.  { x  | 
ph }  <->  [ x  /  x ] ph )
2 sbid 1863 . 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 1629    e. wcel 1684   {cab 2269
This theorem is referenced by:  abeq2  2388  abeq2i  2390  abeq1i  2391  abeq2d  2392  abid2f  2444  elabgt  2911  elabgf  2912  ralab2  2930  rexab2  2932  sbccsbg  3109  sbccsb2g  3110  ss2ab  3241  abn0  3473  tpid3g  3741  eluniab  3839  elintab  3873  iunab  3948  iinab  3963  zfrep4  4139  finds2  4684  sniota  5246  eloprabga  5934  opabiota  6293  eusvobj2  6337  en3lplem2  7417  scottexs  7557  scott0s  7558  cp  7561  cardprclem  7612  cfflb  7885  fin23lem29  7967  axdc3lem2  8077  4sqlem12  13003  xkococn  17354  ptcmplem4  17749  ballotth  23096  abeq2f  23129  rabid2f  23135  ssiun3  23156  ofrn2  23207  sigaclcuni  23479  sigaclcu2  23481  ellines  24775  dominc  25280  rninc  25281  setindtrs  27118  compab  27644  tpid3gVD  28618  en3lplem2VD  28620  bnj1143  28822  bnj1366  28862  bnj906  28962  bnj1256  29045  bnj1259  29046  bnj1311  29054
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-sb 1630  df-clab 2270
  Copyright terms: Public domain W3C validator