Theorem abid 2127

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

Syntax hints:   <-> wb 104   e. wcel 1480   [wsb 1735   {cab 2125

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 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-4 1487  ax-17 1506  ax-i9 1510

This theorem depends on definitions:  df-bi 116  df-sb 1736  df-clab 2126

This theorem is referenced by:  abeq2  2248  abeq2i  2250  abeq1i  2251  abeq2d  2252  abid2f  2306  elabgt  2825  elabgf  2826  ralab2  2848  rexab2  2850  sbccsbg  3031  sbccsb2g  3032  ss2ab  3165  abn0r  3387  abn0m  3388  tpid3g  3638  eluniab  3748  elintab  3782  iunab  3859  iinab  3874  intexabim  4077  iinexgm  4079  opm  4156  finds2  4515  dmmrnm  4758  sniota  5115  eusvobj2  5760  eloprabga  5858  indpi  7150  elabgf0  12984