Theorem abid 2610

Description: Simplification of class abstraction notation when the free and bound variables are identical. (Contributed by NM, 26-May-1993.)

Assertion

Ref	Expression
abid	|- ( x e. { x | ph } <-> ph )

Proof of Theorem abid

Step	Hyp	Ref	Expression
1		df-clab 2609	. 2 |- ( x e. { x | ph } <-> [ x / x ] ph )
2		sbid 2114	. 2 |- ( [ x / x ] ph <-> ph )
3	1, 2	bitri 264	1 |- ( x e. { x | ph } <-> ph )

Syntax hints:   <-> wb 196   [wsb 1880   e. wcel 1990   {cab 2608

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-sb 1881  df-clab 2609

This theorem is referenced by:  abeq2  2732  abeq2d  2734  abbi  2737  abid2f  2791  abeq2f  2792  elabgt  3347  elabgf  3348  ralab2  3371  rexab2  3373  ss2ab  3670  ab0  3951  abn0  3954  sbccsb  4004  sbccsb2  4005  tpid3gOLD  4306  eluniab  4447  elintab  4487  iunab  4566  iinab  4581  zfrep4  4779  sniota  5878  opabiota  6261  eusvobj2  6643  eloprabga  6747  finds2  7094  wfrlem12  7426  en3lplem2  8512  scottexs  8750  scott0s  8751  cp  8754  cardprclem  8805  cfflb  9081  fin23lem29  9163  axdc3lem2  9273  4sqlem12  15660  xkococn  21463  ptcmplem4  21859  ofpreima  29465  qqhval2  30026  esum2dlem  30154  sigaclcu2  30183  bnj1143  30861  bnj1366  30900  bnj906  31000  bnj1256  31083  bnj1259  31084  bnj1311  31092  mclsax  31466  ellines  32259  bj-abeq2  32773  bj-csbsnlem  32898  topdifinffinlem  33195  finxpreclem6  33233  finxpnom  33238  setindtrs  37592  rababg  37879  compab  38645  tpid3gVD  39077  en3lplem2VD  39079  iunmapsn  39409  ssfiunibd  39523  setrec2lem2  42441