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

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

Syntax hints:   ↔ wb 206  [wsb 2064   ∈ wcel 2108  {cab 2713

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 2007  ax-12 2177

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

This theorem is referenced by:  eqabbOLD  2875  eqabrd  2877  eqabf  2928  abid2fOLD  2930  elabgf  3653  ralab2  3680  rexab2  3682  ss2ab  4037  ab0ALT  4356  sbccsb  4411  sbccsb2  4412  eluniab  4897  elintabOLD  4935  iunab  5027  iinab  5044  zfrep4  5263  rnep  5906  sniota  6522  opabiota  6961  eusvobj2  7397  eloprabga  7516  finds2  7894  frrlem10  8294  wfrlem12OLD  8334  en3lplem2  9627  scottexs  9901  scott0s  9902  cp  9905  cardprclem  9993  cfflb  10273  fin23lem29  10355  axdc3lem2  10465  4sqlem12  16976  xkococn  23598  ptcmplem4  23993  noinfbnd1lem1  27687  ofpreima  32643  algextdeglem6  33756  qqhval2  34013  esum2dlem  34123  sigaclcu2  34151  bnj1143  34821  bnj1366  34860  bnj906  34961  bnj1256  35046  bnj1259  35047  bnj1311  35055  mclsax  35591  ellines  36170  bj-csbsnlem  36921  bj-reabeq  37045  bj-velpwALT  37071  topdifinffinlem  37365  rdgssun  37396  finxpreclem6  37414  finxpnom  37419  ralssiun  37425  setindtrs  43049  rababg  43598  scottabf  44264  compab  44466  tpid3gVD  44866  en3lplem2VD  44868  permaxrep  45031  iunmapsn  45241  ssfiunibd  45338  absnsb  47056  setrec2lem2  49558