Theorem abid 2711

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

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

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 2708

This theorem is referenced by:  eqabbOLD  2868  eqabrd  2870  eqabf  2921  abid2fOLD  2923  elabgf  3641  ralab2  3668  rexab2  3670  ss2ab  4025  ab0ALT  4344  sbccsb  4399  sbccsb2  4400  eluniab  4885  elintabOLD  4923  iunab  5015  iinab  5032  zfrep4  5248  rnep  5890  sniota  6502  opabiota  6943  eusvobj2  7379  eloprabga  7498  finds2  7874  frrlem10  8274  en3lplem2  9566  scottexs  9840  scott0s  9841  cp  9844  cardprclem  9932  cfflb  10212  fin23lem29  10294  axdc3lem2  10404  4sqlem12  16927  xkococn  23547  ptcmplem4  23942  noinfbnd1lem1  27635  ofpreima  32589  algextdeglem6  33712  qqhval2  33972  esum2dlem  34082  sigaclcu2  34110  bnj1143  34780  bnj1366  34819  bnj906  34920  bnj1256  35005  bnj1259  35006  bnj1311  35014  mclsax  35556  ellines  36140  bj-csbsnlem  36891  bj-reabeq  37015  bj-velpwALT  37041  topdifinffinlem  37335  rdgssun  37366  finxpreclem6  37384  finxpnom  37389  ralssiun  37395  setindtrs  43014  rababg  43563  scottabf  44229  compab  44431  tpid3gVD  44831  en3lplem2VD  44833  permaxrep  44996  iunmapsn  45211  ssfiunibd  45307  absnsb  47028  setrec2lem2  49683