Theorem abid 2069

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

Syntax hints:   <-> wb 103   e. wcel 1433   [wsb 1685   {cab 2067

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-4 1440  ax-17 1459  ax-i9 1463

This theorem depends on definitions:  df-bi 115  df-sb 1686  df-clab 2068

This theorem is referenced by:  abeq2  2187  abeq2i  2189  abeq1i  2190  abeq2d  2191  abid2f  2243  elabgt  2735  elabgf  2736  ralab2  2756  rexab2  2758  sbccsbg  2934  sbccsb2g  2935  ss2ab  3062  abn0r  3270  tpid3g  3505  eluniab  3613  elintab  3647  iunab  3724  iinab  3739  intexabim  3927  iinexgm  3929  opm  3989  finds2  4342  dmmrnm  4572  sniota  4914  eusvobj2  5518  eloprabga  5611  indpi  6532  elabgf0  10587