Theorem abid 2195

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

Syntax hints:   <-> wb 105   [wsb 1786   e. wcel 2178   {cab 2193

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 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-4 1534  ax-17 1550  ax-i9 1554

This theorem depends on definitions:  df-bi 117  df-sb 1787  df-clab 2194

This theorem is referenced by:  abeq2  2316  abeq2i  2318  abeq1i  2319  abeq2d  2320  abid2f  2376  elabgt  2921  elabgf  2922  ralab2  2944  rexab2  2946  sbccsbg  3130  sbccsb2g  3131  ss2ab  3269  abn0r  3493  abn0m  3494  tpid3g  3758  eluniab  3876  elintab  3910  iunab  3988  iinab  4003  intexabim  4212  iinexgm  4214  opm  4296  finds2  4667  dmmrnm  4916  iotaexab  5269  sniota  5281  eusvobj2  5953  eloprabga  6055  indpi  7490  4sqlem12  12840  elabgf0  15913