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

Theorem abid 2177
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 2176 . 2 (𝑥 ∈ {𝑥𝜑} ↔ [𝑥 / 𝑥]𝜑)
2 sbid 1785 . 2 ([𝑥 / 𝑥]𝜑𝜑)
31, 2bitri 184 1 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
Colors of variables: wff set class
Syntax hints:  wb 105  [wsb 1773  wcel 2160  {cab 2175
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-4 1521  ax-17 1537  ax-i9 1541
This theorem depends on definitions:  df-bi 117  df-sb 1774  df-clab 2176
This theorem is referenced by:  abeq2  2298  abeq2i  2300  abeq1i  2301  abeq2d  2302  abid2f  2358  elabgt  2893  elabgf  2894  ralab2  2916  rexab2  2918  sbccsbg  3101  sbccsb2g  3102  ss2ab  3238  abn0r  3462  abn0m  3463  tpid3g  3725  eluniab  3839  elintab  3873  iunab  3951  iinab  3966  intexabim  4173  iinexgm  4175  opm  4255  finds2  4621  dmmrnm  4867  iotaexab  5217  sniota  5229  eusvobj2  5886  eloprabga  5987  indpi  7376  4sqlem12  12445  elabgf0  15015
  Copyright terms: Public domain W3C validator