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

Theorem abid 2103
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 2102 . 2  |-  ( x  e.  { x  | 
ph }  <->  [ x  /  x ] ph )
2 sbid 1730 . 2  |-  ( [ x  /  x ] ph 
<-> 
ph )
31, 2bitri 183 1  |-  ( x  e.  { x  | 
ph }  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 104    e. wcel 1463   [wsb 1718   {cab 2101
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-4 1470  ax-17 1489  ax-i9 1493
This theorem depends on definitions:  df-bi 116  df-sb 1719  df-clab 2102
This theorem is referenced by:  abeq2  2224  abeq2i  2226  abeq1i  2227  abeq2d  2228  abid2f  2281  elabgt  2797  elabgf  2798  ralab2  2819  rexab2  2821  sbccsbg  2999  sbccsb2g  3000  ss2ab  3133  abn0r  3355  abn0m  3356  tpid3g  3606  eluniab  3716  elintab  3750  iunab  3827  iinab  3842  intexabim  4045  iinexgm  4047  opm  4124  finds2  4483  dmmrnm  4726  sniota  5083  eusvobj2  5726  eloprabga  5824  indpi  7114  elabgf0  12786
  Copyright terms: Public domain W3C validator