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

Theorem abid 2010
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 {xφ} ↔ φ)

Proof of Theorem abid
StepHypRef Expression
1 df-clab 2009 . 2 (x {xφ} ↔ [x / x]φ)
2 sbid 1639 . 2 ([x / x]φφ)
31, 2bitri 173 1 (x {xφ} ↔ φ)
Colors of variables: wff set class
Syntax hints:  wb 98   wcel 1374  [wsb 1627  {cab 2008
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-4 1381  ax-17 1400  ax-i9 1404
This theorem depends on definitions:  df-bi 110  df-sb 1628  df-clab 2009
This theorem is referenced by:  abeq2  2128  abeq2i  2130  abeq1i  2131  abeq2d  2132  abid2f  2184  elabgt  2661  elabgf  2662  ralab2  2682  rexab2  2684  sbccsbg  2855  sbccsb2g  2856  ss2ab  2985  abn0r  3220  tpid3g  3457  eluniab  3566  elintab  3600  iunab  3677  iinab  3692  intexabim  3880  iinexgm  3882  opm  3945  finds2  4251  dmmrnm  4481  sniota  4821  eusvobj2  5422  eloprabga  5514  elabgf0  7170
  Copyright terms: Public domain W3C validator