Theorem abid 2713

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

Syntax hints:   ↔ wb 206  [wsb 2067   ∈ wcel 2111  {cab 2709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2180

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710

This theorem is referenced by:  eqabbOLD  2871  eqabrd  2873  eqabf  2924  abid2fOLD  2926  elabgf  3630  ralab2  3656  rexab2  3658  ss2ab  4013  ab0ALT  4331  sbccsb  4386  sbccsb2  4387  eluniab  4873  iunab  5000  iinab  5016  zfrep4  5231  rnep  5867  sniota  6472  opabiota  6904  eusvobj2  7338  eloprabga  7455  finds2  7828  frrlem10  8225  en3lplem2  9503  scottexs  9780  scott0s  9781  cp  9784  cardprclem  9872  cfflb  10150  fin23lem29  10232  axdc3lem2  10342  4sqlem12  16868  xkococn  23576  ptcmplem4  23971  noinfbnd1lem1  27663  ofpreima  32645  algextdeglem6  33733  qqhval2  33993  esum2dlem  34103  sigaclcu2  34131  bnj1143  34800  bnj1366  34839  bnj906  34940  bnj1256  35025  bnj1259  35026  bnj1311  35034  mclsax  35611  ellines  36192  bj-csbsnlem  36943  bj-reabeq  37067  bj-velpwALT  37093  topdifinffinlem  37387  rdgssun  37418  finxpreclem6  37436  finxpnom  37441  ralssiun  37447  setindtrs  43064  rababg  43613  scottabf  44279  compab  44480  tpid3gVD  44880  en3lplem2VD  44882  permaxrep  45045  iunmapsn  45260  ssfiunibd  45356  absnsb  47064  setrec2lem2  49732