Theorem abid 2712

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 2709	. 2 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ [𝑥 / 𝑥]𝜑)
2		sbid 2256	. 2 ⊢ ([𝑥 / 𝑥]𝜑 ↔ 𝜑)
3	1, 2	bitri 275	1 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)

Syntax hints:   ↔ wb 206  [wsb 2065   ∈ wcel 2109  {cab 2708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709

This theorem is referenced by:  eqabbOLD  2869  eqabrd  2871  eqabf  2922  abid2fOLD  2924  elabgf  3644  ralab2  3671  rexab2  3673  ss2ab  4028  ab0ALT  4347  sbccsb  4402  sbccsb2  4403  eluniab  4888  elintabOLD  4926  iunab  5018  iinab  5035  zfrep4  5251  rnep  5893  sniota  6505  opabiota  6946  eusvobj2  7382  eloprabga  7501  finds2  7877  frrlem10  8277  en3lplem2  9573  scottexs  9847  scott0s  9848  cp  9851  cardprclem  9939  cfflb  10219  fin23lem29  10301  axdc3lem2  10411  4sqlem12  16934  xkococn  23554  ptcmplem4  23949  noinfbnd1lem1  27642  ofpreima  32596  algextdeglem6  33719  qqhval2  33979  esum2dlem  34089  sigaclcu2  34117  bnj1143  34787  bnj1366  34826  bnj906  34927  bnj1256  35012  bnj1259  35013  bnj1311  35021  mclsax  35563  ellines  36147  bj-csbsnlem  36898  bj-reabeq  37022  bj-velpwALT  37048  topdifinffinlem  37342  rdgssun  37373  finxpreclem6  37391  finxpnom  37396  ralssiun  37402  setindtrs  43021  rababg  43570  scottabf  44236  compab  44438  tpid3gVD  44838  en3lplem2VD  44840  permaxrep  45003  iunmapsn  45218  ssfiunibd  45314  absnsb  47032  setrec2lem2  49687