Theorem abid 2177

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 2176	. 2 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ [𝑥 / 𝑥]𝜑)
2		sbid 1785	. 2 ⊢ ([𝑥 / 𝑥]𝜑 ↔ 𝜑)
3	1, 2	bitri 184	1 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)

Syntax hints:   ↔ wb 105  [wsb 1773   ∈ wcel 2160  {cab 2175

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-4 1521  ax-17 1537  ax-i9 1541

This theorem depends on definitions:  df-bi 117  df-sb 1774  df-clab 2176

This theorem is referenced by:  abeq2  2298  abeq2i  2300  abeq1i  2301  abeq2d  2302  abid2f  2358  elabgt  2893  elabgf  2894  ralab2  2916  rexab2  2918  sbccsbg  3101  sbccsb2g  3102  ss2ab  3238  abn0r  3462  abn0m  3463  tpid3g  3725  eluniab  3839  elintab  3873  iunab  3951  iinab  3966  intexabim  4173  iinexgm  4175  opm  4255  finds2  4621  dmmrnm  4867  iotaexab  5217  sniota  5229  eusvobj2  5886  eloprabga  5987  indpi  7376  4sqlem12  12445  elabgf0  15015