Theorem abid 2158

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

Assertion

Ref	Expression
abid	⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)

Proof of Theorem abid

Step	Hyp	Ref	Expression
1		df-clab 2157	. 2 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ [𝑥 / 𝑥]𝜑)
2		sbid 1767	. 2 ⊢ ([𝑥 / 𝑥]𝜑 ↔ 𝜑)
3	1, 2	bitri 183	1 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)

Syntax hints:   ↔ wb 104  [wsb 1755   ∈ wcel 2141  {cab 2156

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-4 1503  ax-17 1519  ax-i9 1523

This theorem depends on definitions:  df-bi 116  df-sb 1756  df-clab 2157

This theorem is referenced by:  abeq2  2279  abeq2i  2281  abeq1i  2282  abeq2d  2283  abid2f  2338  elabgt  2871  elabgf  2872  ralab2  2894  rexab2  2896  sbccsbg  3078  sbccsb2g  3079  ss2ab  3215  abn0r  3439  abn0m  3440  tpid3g  3698  eluniab  3808  elintab  3842  iunab  3919  iinab  3934  intexabim  4138  iinexgm  4140  opm  4219  finds2  4585  dmmrnm  4830  sniota  5189  eusvobj2  5839  eloprabga  5940  indpi  7304  elabgf0  13812