Theorem abid 1465

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

Syntax hints:   <-> wb 146   e. wcel 958  [wsbc 1170  {cab 1463

This theorem is referenced by:  abeq2 1568  abeq2i 1570  abeq1i 1571  abeq2d 1572  eq2ab 1573  elabgt 1895  elabf 1896  elabgf 1898  cbvab 1908  sbccsbg 2022  sbccsb2g 2023  ss2ab 2116  abn0 2290  eluniab 2513  elintab 2544  ssintab 2550  zfrep4 2701  euuni 2881  reucl 2885  onminex 3020  finds2 3158  iunon 3909  iinon 3910  eloprabg 4007  iunfiOLD 4569  scott0 4717  scottexs 4718  scott0s 4719  cp 4722  ac6lem 4754

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-12 968  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464

Copyright terms: Public domain