Theorem abid 2722

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

Syntax hints:   ↔ wb 207  [wsb 2073   ∈ wcel 2119  {cab 2718

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719

This theorem is referenced by:  eqabrd  2881  eqabf  2931  abid2fOLD  2933  elabgf  3619  ralab2  3645  rexab2  3647  ss2ab  3999  ab0ALT  4316  sbccsb  4371  sbccsb2  4372  eluniab  4859  iunab  4988  iinab  5004  zfrep4  5222  rnep  5876  sniota  6483  opabiota  6916  eusvobj2  7355  eloprabga  7472  finds2  7845  frrlem10  8242  en3lplem2  9532  scottexs  9809  scott0s  9810  cp  9813  cardprclem  9901  cfflb  10179  fin23lem29  10261  axdc3lem2  10371  4sqlem12  16925  xkococn  23650  ptcmplem4  24045  noinfbnd1lem1  27712  ofpreima  32764  algextdeglem6  33913  qqhval2  34173  esum2dlem  34283  sigaclcu2  34311  bnj1143  34979  bnj1366  35018  bnj906  35119  bnj1256  35204  bnj1259  35205  bnj1311  35213  mclsax  35804  ellines  36387  bj-csbsnlem  37263  bj-reabeq  37387  bj-velpwALT  37413  topdifinffinlem  37716  rdgssun  37747  finxpreclem6  37765  finxpnom  37770  ralssiun  37776  setindtrs  43477  rababg  44025  scottabf  44691  compab  44892  tpid3gVD  45292  en3lplem2VD  45294  permaxrep  45457  iunmapsn  45669  ssfiunibd  45764  absnsb  47497  setrec2lem2  50191