Theorem abid 2716

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

Syntax hints:   ↔ wb 206  [wsb 2062   ∈ wcel 2106  {cab 2712

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-12 2175

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713

This theorem is referenced by:  eqabbOLD  2880  eqabrd  2882  eqabf  2933  abid2fOLD  2935  elabgtOLDOLD  3674  elabgf  3675  elabgOLD  3678  ralab2  3706  rexab2  3708  ss2ab  4072  ab0ALT  4387  sbccsb  4442  sbccsb2  4443  eluniab  4926  elintabOLD  4964  iunab  5056  iinab  5073  zfrep4  5299  rnep  5940  sniota  6554  opabiota  6991  eusvobj2  7423  eloprabga  7541  eloprabgaOLD  7542  finds2  7921  frrlem10  8319  wfrlem12OLD  8359  en3lplem2  9651  scottexs  9925  scott0s  9926  cp  9929  cardprclem  10017  cfflb  10297  fin23lem29  10379  axdc3lem2  10489  4sqlem12  16990  xkococn  23684  ptcmplem4  24079  noinfbnd1lem1  27783  ofpreima  32682  algextdeglem6  33728  qqhval2  33945  esum2dlem  34073  sigaclcu2  34101  bnj1143  34783  bnj1366  34822  bnj906  34923  bnj1256  35008  bnj1259  35009  bnj1311  35017  mclsax  35554  ellines  36134  bj-csbsnlem  36886  bj-reabeq  37010  bj-velpwALT  37036  topdifinffinlem  37330  rdgssun  37361  finxpreclem6  37379  finxpnom  37384  ralssiun  37390  setindtrs  43014  rababg  43564  scottabf  44236  compab  44438  tpid3gVD  44840  en3lplem2VD  44842  iunmapsn  45160  ssfiunibd  45260  absnsb  46977  setrec2lem2  48925