Theorem abid 2217

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

Syntax hints:   <-> wb 105   [wsb 1808   e. wcel 2200   {cab 2215

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 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-4 1556  ax-17 1572  ax-i9 1576

This theorem depends on definitions:  df-bi 117  df-sb 1809  df-clab 2216

This theorem is referenced by:  abeq2  2338  abeq2i  2340  abeq1i  2341  abeq2d  2342  abid2f  2398  elabgt  2944  elabgf  2945  ralab2  2967  rexab2  2969  sbccsbg  3153  sbccsb2g  3154  ss2ab  3292  abn0r  3516  abn0m  3517  tpid3g  3782  eluniab  3900  elintab  3934  iunab  4012  iinab  4027  intexabim  4236  iinexgm  4238  opm  4320  finds2  4693  dmmrnm  4943  iotaexab  5297  sniota  5309  eusvobj2  5987  eloprabga  6091  indpi  7529  4sqlem12  12925  elabgf0  16141