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

Theorem abid 2073
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 2072 . 2  |-  ( x  e.  { x  | 
ph }  <->  [ x  /  x ] ph )
2 sbid 1701 . 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 1436   [wsb 1689   {cab 2071
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 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-4 1443  ax-17 1462  ax-i9 1466
This theorem depends on definitions:  df-bi 115  df-sb 1690  df-clab 2072
This theorem is referenced by:  abeq2  2193  abeq2i  2195  abeq1i  2196  abeq2d  2197  abid2f  2249  elabgt  2748  elabgf  2749  ralab2  2770  rexab2  2772  sbccsbg  2948  sbccsb2g  2949  ss2ab  3078  abn0r  3296  abn0m  3297  tpid3g  3540  eluniab  3650  elintab  3684  iunab  3761  iinab  3776  intexabim  3965  iinexgm  3967  opm  4037  finds2  4391  dmmrnm  4625  sniota  4975  eusvobj2  5601  eloprabga  5694  indpi  6848  elabgf0  11165
  Copyright terms: Public domain W3C validator