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

Theorem abid 2044
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 2043 . 2 (𝑥 ∈ {𝑥𝜑} ↔ [𝑥 / 𝑥]𝜑)
2 sbid 1673 . 2 ([𝑥 / 𝑥]𝜑𝜑)
31, 2bitri 177 1 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
Colors of variables: wff set class
Syntax hints:  wb 102  wcel 1409  [wsb 1661  {cab 2042
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-4 1416  ax-17 1435  ax-i9 1439
This theorem depends on definitions:  df-bi 114  df-sb 1662  df-clab 2043
This theorem is referenced by:  abeq2  2162  abeq2i  2164  abeq1i  2165  abeq2d  2166  abid2f  2218  elabgt  2707  elabgf  2708  ralab2  2728  rexab2  2730  sbccsbg  2906  sbccsb2g  2907  ss2ab  3036  abn0r  3271  tpid3g  3511  eluniab  3620  elintab  3654  iunab  3731  iinab  3746  intexabim  3934  iinexgm  3936  opm  3999  finds2  4352  dmmrnm  4582  sniota  4922  eusvobj2  5526  eloprabga  5619  indpi  6498  elabgf0  10303
  Copyright terms: Public domain W3C validator