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  2945  elabgf  2946  ralab2  2968  rexab2  2970  sbccsbg  3154  sbccsb2g  3155  ss2ab  3293  abn0r  3517  abn0m  3518  tpid3g  3785  eluniab  3903  elintab  3937  iunab  4015  iinab  4030  intexabim  4240  iinexgm  4242  opm  4324  finds2  4697  dmmrnm  4949  iotaexab  5303  sniota  5315  eusvobj2  5999  eloprabga  6103  modom  6989  indpi  7552  4sqlem12  12965  elabgf0  16309