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

Theorem abid 2181
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 2180 . 2 (𝑥 ∈ {𝑥𝜑} ↔ [𝑥 / 𝑥]𝜑)
2 sbid 1785 . 2 ([𝑥 / 𝑥]𝜑𝜑)
31, 2bitri 184 1 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
Colors of variables: wff set class
Syntax hints:  wb 105  [wsb 1773  wcel 2164  {cab 2179
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 2180
This theorem is referenced by:  abeq2  2302  abeq2i  2304  abeq1i  2305  abeq2d  2306  abid2f  2362  elabgt  2902  elabgf  2903  ralab2  2925  rexab2  2927  sbccsbg  3110  sbccsb2g  3111  ss2ab  3248  abn0r  3472  abn0m  3473  tpid3g  3734  eluniab  3848  elintab  3882  iunab  3960  iinab  3975  intexabim  4182  iinexgm  4184  opm  4264  finds2  4634  dmmrnm  4882  iotaexab  5234  sniota  5246  eusvobj2  5905  eloprabga  6006  indpi  7404  4sqlem12  12543  elabgf0  15339
  Copyright terms: Public domain W3C validator