Theorem abid 2153

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 2152	. 2 |- ( x e. { x | ph } <-> [ x / x ] ph )
2		sbid 1762	. 2 |- ( [ x / x ] ph <-> ph )
3	1, 2	bitri 183	1 |- ( x e. { x | ph } <-> ph )

Syntax hints:   <-> wb 104   [wsb 1750   e. wcel 2136   {cab 2151

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-4 1498  ax-17 1514  ax-i9 1518

This theorem depends on definitions:  df-bi 116  df-sb 1751  df-clab 2152

This theorem is referenced by:  abeq2  2275  abeq2i  2277  abeq1i  2278  abeq2d  2279  abid2f  2334  elabgt  2867  elabgf  2868  ralab2  2890  rexab2  2892  sbccsbg  3074  sbccsb2g  3075  ss2ab  3210  abn0r  3433  abn0m  3434  tpid3g  3691  eluniab  3801  elintab  3835  iunab  3912  iinab  3927  intexabim  4131  iinexgm  4133  opm  4212  finds2  4578  dmmrnm  4823  sniota  5180  eusvobj2  5828  eloprabga  5929  indpi  7283  elabgf0  13658