Theorem abid 2025

Description: Simplification of class abstraction notation when the free and bound variables are identical. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
abid	|- (x e. {x | ph } <-> ph)

Proof of Theorem abid

Step	Hyp	Ref	Expression
1		df-clab 2024	. 2 |- (x e. {x | ph } <-> [x / x]ph)
2		sbid 1654	. 2 |- ([x / x]ph <-> ph)
3	1, 2	bitri 173	1 |- (x e. {x | ph } <-> ph)

Syntax hints:   <-> wb 98   e. wcel 1390  [wsb 1642   {cab 2023

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-4 1397  ax-17 1416  ax-i9 1420

This theorem depends on definitions:  df-bi 110  df-sb 1643  df-clab 2024

This theorem is referenced by:  abeq2  2143  abeq2i  2145  abeq1i  2146  abeq2d  2147  abid2f  2199  elabgt  2678  elabgf  2679  ralab2  2699  rexab2  2701  sbccsbg  2872  sbccsb2g  2873  ss2ab  3002  abn0r  3237  tpid3g  3474  eluniab  3583  elintab  3617  iunab  3694  iinab  3709  intexabim  3897  iinexgm  3899  opm  3962  finds2  4267  dmmrnm  4497  sniota  4837  eusvobj2  5441  eloprabga  5533  indpi  6326  elabgf0  9231