Theorem abid 2721

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

Syntax hints:   ↔ wb 206  [wsb 2064   ∈ wcel 2108  {cab 2717

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718

This theorem is referenced by:  eqabbOLD  2885  eqabrd  2887  eqabf  2941  abid2fOLD  2943  elabgtOLDOLD  3687  elabgf  3688  elabgOLD  3691  ralab2  3719  rexab2  3721  ss2ab  4085  ab0ALT  4404  sbccsb  4459  sbccsb2  4460  eluniab  4945  elintabOLD  4983  iunab  5074  iinab  5091  zfrep4  5314  rnep  5951  sniota  6564  opabiota  7004  eusvobj2  7440  eloprabga  7558  eloprabgaOLD  7559  finds2  7938  frrlem10  8336  wfrlem12OLD  8376  en3lplem2  9682  scottexs  9956  scott0s  9957  cp  9960  cardprclem  10048  cfflb  10328  fin23lem29  10410  axdc3lem2  10520  4sqlem12  17003  xkococn  23689  ptcmplem4  24084  noinfbnd1lem1  27786  ofpreima  32683  algextdeglem6  33713  qqhval2  33928  esum2dlem  34056  sigaclcu2  34084  bnj1143  34766  bnj1366  34805  bnj906  34906  bnj1256  34991  bnj1259  34992  bnj1311  35000  mclsax  35537  ellines  36116  bj-csbsnlem  36869  bj-reabeq  36993  bj-velpwALT  37019  topdifinffinlem  37313  rdgssun  37344  finxpreclem6  37362  finxpnom  37367  ralssiun  37373  setindtrs  42982  rababg  43536  scottabf  44209  compab  44411  tpid3gVD  44813  en3lplem2VD  44815  iunmapsn  45124  ssfiunibd  45224  absnsb  46942  setrec2lem2  48786