Theorem abid 2609

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

Syntax hints:   ↔ wb 196  [wsb 1877   ∈ wcel 1987  {cab 2607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-12 2044

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-sb 1878  df-clab 2608

This theorem is referenced by:  abeq2  2729  abeq2d  2731  abbi  2734  abid2f  2787  abeq2f  2788  elabgt  3335  elabgf  3336  ralab2  3358  rexab2  3360  ss2ab  3655  ab0  3931  abn0  3934  sbccsb  3982  sbccsb2  3983  tpid3gOLD  4283  eluniab  4420  elintab  4459  iunab  4539  iinab  4554  zfrep4  4749  sniota  5847  opabiota  6228  eusvobj2  6608  eloprabga  6712  finds2  7056  wfrlem12  7386  en3lplem2  8472  scottexs  8710  scott0s  8711  cp  8714  cardprclem  8765  cfflb  9041  fin23lem29  9123  axdc3lem2  9233  4sqlem12  15603  xkococn  21403  ptcmplem4  21799  ofpreima  29349  qqhval2  29850  esum2dlem  29977  sigaclcu2  30006  bnj1143  30622  bnj1366  30661  bnj906  30761  bnj1256  30844  bnj1259  30845  bnj1311  30853  mclsax  31227  ellines  31954  bj-abeq2  32469  bj-csbsnlem  32598  topdifinffinlem  32866  finxpreclem6  32904  finxpnom  32909  setindtrs  37111  rababg  37399  compab  38166  tpid3gVD  38599  en3lplem2VD  38601  iunmapsn  38918  ssfiunibd  39022  setrec2lem2  41764