MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  abid Structured version   Visualization version   GIF version

Theorem abid 2717
Description: Simplification of class abstraction notation when the free and bound variables are identical. (Contributed by NM, 26-May-1993.)
Assertion
Ref Expression
abid (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)

Proof of Theorem abid
StepHypRef Expression
1 df-clab 2714 . 2 (𝑥 ∈ {𝑥𝜑} ↔ [𝑥 / 𝑥]𝜑)
2 sbid 2247 . 2 ([𝑥 / 𝑥]𝜑𝜑)
31, 2bitri 274 1 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 205  [wsb 2067  wcel 2106  {cab 2713
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2714
This theorem is referenced by:  eqabOLD  2878  eqabd  2880  abid2f  2939  eqabf  2940  elabgtOLD  3625  elabgf  3626  elabgOLD  3629  ralab2  3655  rexab2  3657  ss2ab  4016  ab0ALT  4336  abn0OLD  4341  sbccsb  4393  sbccsb2  4394  eluniab  4880  elintabOLD  4920  iunab  5011  iinab  5028  zfrep4  5253  rnep  5882  sniota  6487  opabiota  6924  eusvobj2  7349  eloprabga  7464  eloprabgaOLD  7465  finds2  7837  frrlem10  8226  wfrlem12OLD  8266  en3lplem2  9549  scottexs  9823  scott0s  9824  cp  9827  cardprclem  9915  cfflb  10195  fin23lem29  10277  axdc3lem2  10387  4sqlem12  16828  xkococn  23011  ptcmplem4  23406  noinfbnd1lem1  27071  ofpreima  31581  qqhval2  32563  esum2dlem  32691  sigaclcu2  32719  bnj1143  33402  bnj1366  33441  bnj906  33542  bnj1256  33627  bnj1259  33628  bnj1311  33636  mclsax  34163  ellines  34737  bj-csbsnlem  35370  bj-reabeq  35498  bj-velpwALT  35524  topdifinffinlem  35818  rdgssun  35849  finxpreclem6  35867  finxpnom  35872  ralssiun  35878  setindtrs  41335  rababg  41836  scottabf  42510  compab  42712  tpid3gVD  43114  en3lplem2VD  43116  iunmapsn  43428  ssfiunibd  43533  absnsb  45251  setrec2lem2  47129
  Copyright terms: Public domain W3C validator