Theorem abid 2193

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

Syntax hints:   <-> wb 105   [wsb 1785   e. wcel 2176   {cab 2191

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-4 1533  ax-17 1549  ax-i9 1553

This theorem depends on definitions:  df-bi 117  df-sb 1786  df-clab 2192

This theorem is referenced by:  abeq2  2314  abeq2i  2316  abeq1i  2317  abeq2d  2318  abid2f  2374  elabgt  2914  elabgf  2915  ralab2  2937  rexab2  2939  sbccsbg  3122  sbccsb2g  3123  ss2ab  3261  abn0r  3485  abn0m  3486  tpid3g  3748  eluniab  3862  elintab  3896  iunab  3974  iinab  3989  intexabim  4196  iinexgm  4198  opm  4278  finds2  4649  dmmrnm  4897  iotaexab  5250  sniota  5262  eusvobj2  5930  eloprabga  6032  indpi  7455  4sqlem12  12725  elabgf0  15713