Theorem abid 2751

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

Syntax hints:   ↔ wb 209  [wsb 2097   ∈ wcel 2149  {cab 2747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748

This theorem is referenced by:  eqabrd  2910  eqabf  2960  abid2fOLD  2962  elabgf  3642  ralab2  3669  rexab2  3671  ss2ab  4023  ab0ALT  4344  sbccsb  4407  sbccsb2  4408  eluniab  4890  iunab  5020  iinab  5036  zfrep4  5258  rnep  5918  sniota  6528  opabiota  6964  eusvobj2  7403  eloprabga  7520  finds2  7894  frrlem10  8291  en3lplem2  9581  scottexs  9860  scott0s  9861  scottabf  9865  cp  9876  cardprclem  9964  cfflb  10242  fin23lem29  10324  axdc3lem2  10434  4sqlem12  17015  xkococn  23785  ptcmplem4  24180  noinfbnd1lem1  27852  ofpreima  32950  algextdeglem6  34056  qqhval2  34316  esum2dlem  34426  sigaclcu2  34454  bnj1143  35122  bnj1366  35161  bnj906  35262  bnj1256  35347  bnj1259  35348  bnj1311  35356  mclsax  35959  ellines  36542  bj-csbsnlem  37426  bj-reabeq  37550  bj-velpwALT  37576  topdifinffinlem  37880  rdgssun  37911  finxpreclem6  37929  finxpnom  37934  ralssiun  37940  setindtrs  43643  rababg  44191  compab  45042  tpid3gVD  45441  en3lplem2VD  45443  permaxrep  45606  iunmapsn  45824  ssfiunibd  45919  absnsb  47652  setrec2lem2  50356