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  4881  iunab  5011  iinab  5027  zfrep4  5247  rnep  5907  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  17004  xkococn  23774  ptcmplem4  24169  noinfbnd1lem1  27841  ofpreima  32918  algextdeglem6  34024  qqhval2  34284  esum2dlem  34394  sigaclcu2  34422  bnj1143  35090  bnj1366  35129  bnj906  35230  bnj1256  35315  bnj1259  35316  bnj1311  35324  mclsax  35927  ellines  36510  bj-csbsnlem  37395  bj-reabeq  37519  bj-velpwALT  37545  topdifinffinlem  37848  rdgssun  37879  finxpreclem6  37897  finxpnom  37902  ralssiun  37908  setindtrs  43609  rababg  44157  compab  45010  tpid3gVD  45409  en3lplem2VD  45411  permaxrep  45574  iunmapsn  45792  ssfiunibd  45887  absnsb  47620  setrec2lem2  50324