Theorem abid 2341

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

Syntax hints:   <-> wb 176  [wsb 1648   e. wcel 1710  {cab 2339

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-sb 1649  df-clab 2340

This theorem is referenced by:  abeq2  2458  abeq2i  2460  abeq1i  2461  abeq2d  2462  abid2f  2514  elabgt  2982  elabgf  2983  ralab2  3001  rexab2  3003  sbccsbg  3164  sbccsb2g  3165  ss2ab  3334  abn0  3568  tpid3g  3831  eluniab  3903  elintab  3937  iunab  4012  iinab  4027  sniota  4369  eqop  4611  dfswap2  4741  eloprabga  5578