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

Theorem abid 2025
 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 2024 . 2 (x {xφ} ↔ [x / x]φ)
2 sbid 1654 . 2 ([x / x]φφ)
31, 2bitri 173 1 (x {xφ} ↔ φ)
 Colors of variables: wff set class Syntax hints:   ↔ wb 98   ∈ wcel 1390  [wsb 1642  {cab 2023 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 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-4 1397  ax-17 1416  ax-i9 1420 This theorem depends on definitions:  df-bi 110  df-sb 1643  df-clab 2024 This theorem is referenced by:  abeq2  2143  abeq2i  2145  abeq1i  2146  abeq2d  2147  abid2f  2199  elabgt  2678  elabgf  2679  ralab2  2699  rexab2  2701  sbccsbg  2872  sbccsb2g  2873  ss2ab  3002  abn0r  3237  tpid3g  3474  eluniab  3583  elintab  3617  iunab  3694  iinab  3709  intexabim  3897  iinexgm  3899  opm  3962  finds2  4267  dmmrnm  4497  sniota  4837  eusvobj2  5441  eloprabga  5533  indpi  6326  elabgf0  9231
 Copyright terms: Public domain W3C validator