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

Theorem abid 2028
 Description: Simplification of class abstraction notation when the free and bound variables are identical. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
abid (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)

Proof of Theorem abid
StepHypRef Expression
1 df-clab 2027 . 2 (𝑥 ∈ {𝑥𝜑} ↔ [𝑥 / 𝑥]𝜑)
2 sbid 1657 . 2 ([𝑥 / 𝑥]𝜑𝜑)
31, 2bitri 173 1 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
 Colors of variables: wff set class Syntax hints:   ↔ wb 98   ∈ wcel 1393  [wsb 1645  {cab 2026 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 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-4 1400  ax-17 1419  ax-i9 1423 This theorem depends on definitions:  df-bi 110  df-sb 1646  df-clab 2027 This theorem is referenced by:  abeq2  2146  abeq2i  2148  abeq1i  2149  abeq2d  2150  abid2f  2202  elabgt  2684  elabgf  2685  ralab2  2705  rexab2  2707  sbccsbg  2878  sbccsb2g  2879  ss2ab  3008  abn0r  3243  tpid3g  3483  eluniab  3592  elintab  3626  iunab  3703  iinab  3718  intexabim  3906  iinexgm  3908  opm  3971  finds2  4324  dmmrnm  4554  sniota  4894  eusvobj2  5498  eloprabga  5591  indpi  6440  elabgf0  9916
 Copyright terms: Public domain W3C validator