Theorem abid 1463

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

Assertion

Ref	Expression
abid	⊢ (x ∈ {x∣φ} ↔ φ)

Proof of Theorem abid

Step	Hyp	Ref	Expression
1		df-clab 1462	. 2 ⊢ (x ∈ {x∣φ} ↔ [x / x]φ)
2		sbid 1182	. 2 ⊢ ([x / x]φ ↔ φ)
3	1, 2	bitr 173	1 ⊢ (x ∈ {x∣φ} ↔ φ)

Syntax hints:   ↔ wb 146   ∈ wcel 956  [wsbc 1168  {cab 1461

This theorem is referenced by:  abeq2 1565  abeq2i 1567  abeq1i 1568  abeq2d 1569  eq2ab 1570  elabgt 1891  elabf 1892  elabgf 1894  cbvab 1904  sbccsbg 2018  sbccsb2g 2019  ss2ab 2112  abn0 2286  eluniab 2508  elintab 2539  ssintab 2545  zfrep4 2696  euuni 2876  reucl 2880  onminex 3015  finds2 3153  iunon 3900  iinon 3901  eloprabg 3998  iunfi 4549  scott0 4697  scottexs 4698  scott0s 4699  cp 4702  ac6lem 4734

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-12 966  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462

Copyright terms: Public domain