ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  abid Unicode version

Theorem abid 2070
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 2069 . 2  |-  ( x  e.  { x  | 
ph }  <->  [ x  /  x ] ph )
2 sbid 1698 . 2  |-  ( [ x  /  x ] ph 
<-> 
ph )
31, 2bitri 182 1  |-  ( x  e.  { x  | 
ph }  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 103    e. wcel 1434   [wsb 1686   {cab 2068
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-4 1441  ax-17 1460  ax-i9 1464
This theorem depends on definitions:  df-bi 115  df-sb 1687  df-clab 2069
This theorem is referenced by:  abeq2  2188  abeq2i  2190  abeq1i  2191  abeq2d  2192  abid2f  2244  elabgt  2736  elabgf  2737  ralab2  2757  rexab2  2759  sbccsbg  2935  sbccsb2g  2936  ss2ab  3063  abn0r  3277  tpid3g  3513  eluniab  3621  elintab  3655  iunab  3732  iinab  3747  intexabim  3935  iinexgm  3937  opm  3997  finds2  4350  dmmrnm  4582  sniota  4924  eusvobj2  5529  eloprabga  5622  indpi  6594  elabgf0  10738
  Copyright terms: Public domain W3C validator