Theorem abid 2718

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

Syntax hints:   ↔ wb 206  [wsb 2067   ∈ wcel 2113  {cab 2714

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 2184

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

This theorem is referenced by:  eqabrd  2877  eqabf  2928  abid2fOLD  2930  elabgf  3629  ralab2  3655  rexab2  3657  ss2ab  4013  ab0ALT  4333  sbccsb  4388  sbccsb2  4389  eluniab  4877  iunab  5007  iinab  5023  zfrep4  5238  rnep  5876  sniota  6483  opabiota  6916  eusvobj2  7350  eloprabga  7467  finds2  7840  frrlem10  8237  en3lplem2  9522  scottexs  9799  scott0s  9800  cp  9803  cardprclem  9891  cfflb  10169  fin23lem29  10251  axdc3lem2  10361  4sqlem12  16884  xkococn  23604  ptcmplem4  23999  noinfbnd1lem1  27691  ofpreima  32743  algextdeglem6  33879  qqhval2  34139  esum2dlem  34249  sigaclcu2  34277  bnj1143  34946  bnj1366  34985  bnj906  35086  bnj1256  35171  bnj1259  35172  bnj1311  35180  mclsax  35763  ellines  36346  bj-csbsnlem  37104  bj-reabeq  37228  bj-velpwALT  37254  topdifinffinlem  37548  rdgssun  37579  finxpreclem6  37597  finxpnom  37602  ralssiun  37608  setindtrs  43263  rababg  43811  scottabf  44477  compab  44678  tpid3gVD  45078  en3lplem2VD  45080  permaxrep  45243  iunmapsn  45457  ssfiunibd  45553  absnsb  47269  setrec2lem2  49935