Theorem abid 2711

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

Syntax hints:   ↔ wb 206  [wsb 2065   ∈ wcel 2109  {cab 2707

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708

This theorem is referenced by:  eqabbOLD  2868  eqabrd  2870  eqabf  2921  abid2fOLD  2923  elabgf  3632  ralab2  3659  rexab2  3661  ss2ab  4016  ab0ALT  4334  sbccsb  4389  sbccsb2  4390  eluniab  4875  elintabOLD  4912  iunab  5003  iinab  5020  zfrep4  5235  rnep  5873  sniota  6477  opabiota  6909  eusvobj2  7345  eloprabga  7462  finds2  7838  frrlem10  8235  en3lplem2  9528  scottexs  9802  scott0s  9803  cp  9806  cardprclem  9894  cfflb  10172  fin23lem29  10254  axdc3lem2  10364  4sqlem12  16886  xkococn  23563  ptcmplem4  23958  noinfbnd1lem1  27651  ofpreima  32622  algextdeglem6  33691  qqhval2  33951  esum2dlem  34061  sigaclcu2  34089  bnj1143  34759  bnj1366  34798  bnj906  34899  bnj1256  34984  bnj1259  34985  bnj1311  34993  mclsax  35544  ellines  36128  bj-csbsnlem  36879  bj-reabeq  37003  bj-velpwALT  37029  topdifinffinlem  37323  rdgssun  37354  finxpreclem6  37372  finxpnom  37377  ralssiun  37383  setindtrs  43001  rababg  43550  scottabf  44216  compab  44418  tpid3gVD  44818  en3lplem2VD  44820  permaxrep  44983  iunmapsn  45198  ssfiunibd  45294  absnsb  47015  setrec2lem2  49683