Theorem abid 2747

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

Syntax hints:   ↔ wb 209  [wsb 2093   ∈ wcel 2145  {cab 2743

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-12 2215

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744

This theorem is referenced by:  eqabrd  2906  eqabf  2956  abid2fOLD  2958  elabgf  3636  ralab2  3663  rexab2  3665  ss2ab  4017  ab0ALT  4337  sbccsb  4393  sbccsb2  4394  eluniab  4882  iunab  5012  iinab  5028  zfrep4  5248  rnep  5908  sniota  6516  opabiota  6953  eusvobj2  7392  eloprabga  7509  finds2  7883  frrlem10  8280  en3lplem2  9570  scottexs  9849  scott0s  9850  scottabf  9854  cp  9865  cardprclem  9953  cfflb  10231  fin23lem29  10313  axdc3lem2  10423  4sqlem12  17006  xkococn  23778  ptcmplem4  24173  noinfbnd1lem1  27845  ofpreima  32922  algextdeglem6  34029  qqhval2  34289  esum2dlem  34399  sigaclcu2  34427  bnj1143  35095  bnj1366  35134  bnj906  35235  bnj1256  35320  bnj1259  35321  bnj1311  35329  mclsax  35932  ellines  36515  bj-csbsnlem  37400  bj-reabeq  37524  bj-velpwALT  37550  topdifinffinlem  37853  rdgssun  37884  finxpreclem6  37902  finxpnom  37907  ralssiun  37913  setindtrs  43614  rababg  44162  compab  45015  tpid3gVD  45415  en3lplem2VD  45417  permaxrep  45580  iunmapsn  45791  ssfiunibd  45886  absnsb  47619  setrec2lem2  50323