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

Theorem abid 2088
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 2087 . 2 (𝑥 ∈ {𝑥𝜑} ↔ [𝑥 / 𝑥]𝜑)
2 sbid 1715 . 2 ([𝑥 / 𝑥]𝜑𝜑)
31, 2bitri 183 1 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
Colors of variables: wff set class
Syntax hints:  wb 104  wcel 1448  [wsb 1703  {cab 2086
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-4 1455  ax-17 1474  ax-i9 1478
This theorem depends on definitions:  df-bi 116  df-sb 1704  df-clab 2087
This theorem is referenced by:  abeq2  2208  abeq2i  2210  abeq1i  2211  abeq2d  2212  abid2f  2265  elabgt  2779  elabgf  2780  ralab2  2801  rexab2  2803  sbccsbg  2981  sbccsb2g  2982  ss2ab  3112  abn0r  3334  abn0m  3335  tpid3g  3585  eluniab  3695  elintab  3729  iunab  3806  iinab  3821  intexabim  4017  iinexgm  4019  opm  4094  finds2  4453  dmmrnm  4696  sniota  5051  eusvobj2  5692  eloprabga  5790  indpi  7051  elabgf0  12565
  Copyright terms: Public domain W3C validator