Theorem abid 2145

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

Syntax hints:   <-> wb 104   [wsb 1742   e. wcel 2128   {cab 2143

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 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-4 1490  ax-17 1506  ax-i9 1510

This theorem depends on definitions:  df-bi 116  df-sb 1743  df-clab 2144

This theorem is referenced by:  abeq2  2266  abeq2i  2268  abeq1i  2269  abeq2d  2270  abid2f  2325  elabgt  2853  elabgf  2854  ralab2  2876  rexab2  2878  sbccsbg  3060  sbccsb2g  3061  ss2ab  3196  abn0r  3418  abn0m  3419  tpid3g  3674  eluniab  3784  elintab  3818  iunab  3895  iinab  3910  intexabim  4113  iinexgm  4115  opm  4194  finds2  4559  dmmrnm  4804  sniota  5161  eusvobj2  5807  eloprabga  5905  indpi  7256  elabgf0  13322