Theorem abid 2745

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

Syntax hints:   ↔ wb 209  [wsb 2096   ∈ wcel 2143  {cab 2741

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742

This theorem is referenced by:  eqabrd  2904  eqabf  2954  abid2fOLD  2956  elabgf  3634  ralab2  3661  rexab2  3663  ss2ab  4016  ab0ALT  4338  sbccsb  4402  sbccsb2  4403  eluniab  4887  iunab  5017  iinab  5033  zfrep4  5255  rnep  5919  sniota  6529  opabiota  6965  eusvobj2  7404  eloprabga  7521  finds2  7896  frrlem10  8293  en3lplem2  9583  scottexs  9862  scott0s  9863  scottabf  9867  cp  9878  cardprclem  9966  cfflb  10244  fin23lem29  10326  axdc3lem2  10436  4sqlem12  17017  xkococn  23798  ptcmplem4  24193  noinfbnd1lem1  27868  ofpreima  32991  algextdeglem6  34093  qqhval2  34353  esum2dlem  34463  sigaclcu2  34491  bnj1143  35159  bnj1366  35198  bnj906  35299  bnj1256  35384  bnj1259  35385  bnj1311  35393  mclsax  36042  ellines  36625  bj-csbsnlem  37519  bj-reabeq  37644  bj-velpwALT  37670  topdifinffinlem  37974  rdgssun  38005  finxpreclem6  38023  finxpnom  38028  ralssiun  38034  setindtrs  43735  rababg  44283  compab  45134  tpid3gVD  45533  en3lplem2VD  45535  permaxrep  45698  iunmapsn  45916  ssfiunibd  46011  absnsb  47747  setrec2lem2  50455