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

Theorem abid 2127
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 2126 . 2 (𝑥 ∈ {𝑥𝜑} ↔ [𝑥 / 𝑥]𝜑)
2 sbid 1747 . 2 ([𝑥 / 𝑥]𝜑𝜑)
31, 2bitri 183 1 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
Colors of variables: wff set class
Syntax hints:  wb 104  wcel 1480  [wsb 1735  {cab 2125
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 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-4 1487  ax-17 1506  ax-i9 1510
This theorem depends on definitions:  df-bi 116  df-sb 1736  df-clab 2126
This theorem is referenced by:  abeq2  2248  abeq2i  2250  abeq1i  2251  abeq2d  2252  abid2f  2306  elabgt  2825  elabgf  2826  ralab2  2848  rexab2  2850  sbccsbg  3031  sbccsb2g  3032  ss2ab  3165  abn0r  3387  abn0m  3388  tpid3g  3638  eluniab  3748  elintab  3782  iunab  3859  iinab  3874  intexabim  4077  iinexgm  4079  opm  4156  finds2  4515  dmmrnm  4758  sniota  5115  eusvobj2  5760  eloprabga  5858  indpi  7162  elabgf0  13068
  Copyright terms: Public domain W3C validator