Theorem abid 1442

Description: Simplification of class abstraction notation when the free and bound variables are identical.

Assertion

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

Proof of Theorem abid

Step	Hyp	Ref	Expression
1		df-clab 1441	. 2 |- (x e. {x | ph} <-> [x / x]ph)
2		sbid 1167	. 2 |- ([x / x]ph <-> ph)
3	1, 2	bitr 173	1 |- (x e. {x | ph} <-> ph)

Syntax hints:   <-> wb 146   e. wcel 1105  [wsbc 1153  {cab 1440

This theorem is referenced by:  abeq2 1544  abeq2i 1546  abeq1i 1547  abeq2d 1548  eq2ab 1549  elabgt 1867  elabf 1868  elabgf 1870  cbvab 1880  sbccsbg 1993  sbccsb2g 1994  ss2ab 2087  abn0 2261  eluniab 2481  elintab 2512  ssintab 2518  zfrep4 2669  euuni 2844  reucl 2848  onminex 2983  finds2 3121  iunon 3848  iinon 3849  eloprabg 3946  iunfi 4495  scott0 4641  scottexs 4642  scott0s 4643  cp 4646  ac6lem 4678

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-gen 955  ax-9 1102  ax-12 1104

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 957  df-sb 1155  df-clab 1441

Copyright terms: Public domain