Theorem abid 2719

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

Step	Hyp	Ref	Expression
1		df-clab 2716	. 2 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ [𝑥 / 𝑥]𝜑)
2		sbid 2251	. 2 ⊢ ([𝑥 / 𝑥]𝜑 ↔ 𝜑)
3	1, 2	bitri 274	1 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)

Syntax hints:   ↔ wb 205  [wsb 2068   ∈ wcel 2108  {cab 2715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716

This theorem is referenced by:  abeq2  2871  abeq2d  2873  abbiOLD  2879  abid2f  2938  abeq2f  2939  elabgtOLD  3597  elabgf  3598  elabgOLD  3601  ralab2  3627  ralab2OLD  3628  rexab2  3630  rexab2OLD  3631  ss2ab  3989  ab0ALT  4307  abn0OLD  4312  sbccsb  4364  sbccsb2  4365  eluniab  4851  elintab  4887  iunab  4977  iinab  4993  zfrep4  5215  rnep  5825  sniota  6409  opabiota  6833  eusvobj2  7248  eloprabga  7360  eloprabgaOLD  7361  finds2  7721  frrlem10  8082  wfrlem12OLD  8122  en3lplem2  9301  scottexs  9576  scott0s  9577  cp  9580  cardprclem  9668  cfflb  9946  fin23lem29  10028  axdc3lem2  10138  4sqlem12  16585  xkococn  22719  ptcmplem4  23114  ofpreima  30904  qqhval2  31832  esum2dlem  31960  sigaclcu2  31988  bnj1143  32670  bnj1366  32709  bnj906  32810  bnj1256  32895  bnj1259  32896  bnj1311  32904  mclsax  33431  noinfbnd1lem1  33853  ellines  34381  bj-csbsnlem  35015  bj-reabeq  35144  topdifinffinlem  35445  rdgssun  35476  finxpreclem6  35494  finxpnom  35499  ralssiun  35505  setindtrs  40763  rababg  41070  scottabf  41747  compab  41949  tpid3gVD  42351  en3lplem2VD  42353  iunmapsn  42646  ssfiunibd  42738  absnsb  44408  setrec2lem2  46286