Theorem abid 1094

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 1093	. 2 |- (x e. {x | ph} <-> [x / x]ph)
2		sbid 868	. 2 |- ([x / x]ph <-> ph)
3	1, 2	bitr 151	1 |- (x e. {x | ph} <-> ph)

Syntax hints:   <-> wb 127  [wsb 852  {cab 1090   e. wcel 1092

This theorem is referenced by:  cleqab 1174  cleqabi 1176  cleqabri 1177  cleqabd 1178  cleq2ab 1179  elabf 1414  elabgf 1416  cbvab 1423  zfrep4 1479  ss2ab 1551  abn0 1715  eluniab 1926  euuni 1954  reucl 1957  elintab 1976  onminex 2275  finds2 2399  iunon 2947  iinon 2948  eloprabg 3035  scott0 3542  scottexs 3543  scott0s 3544  cp 3547  ac6lem 3575

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677  ax-9 799  ax-12 802

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093

metamath.org