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

Theorem abid 2165
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 2164 . 2 (𝑥 ∈ {𝑥𝜑} ↔ [𝑥 / 𝑥]𝜑)
2 sbid 1774 . 2 ([𝑥 / 𝑥]𝜑𝜑)
31, 2bitri 184 1 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
Colors of variables: wff set class
Syntax hints:  wb 105  [wsb 1762  wcel 2148  {cab 2163
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 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530
This theorem depends on definitions:  df-bi 117  df-sb 1763  df-clab 2164
This theorem is referenced by:  abeq2  2286  abeq2i  2288  abeq1i  2289  abeq2d  2290  abid2f  2345  elabgt  2878  elabgf  2879  ralab2  2901  rexab2  2903  sbccsbg  3086  sbccsb2g  3087  ss2ab  3223  abn0r  3447  abn0m  3448  tpid3g  3707  eluniab  3821  elintab  3855  iunab  3933  iinab  3948  intexabim  4152  iinexgm  4154  opm  4234  finds2  4600  dmmrnm  4846  sniota  5207  eusvobj2  5860  eloprabga  5961  indpi  7340  elabgf0  14499
  Copyright terms: Public domain W3C validator