Theorem abid 2028

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

Syntax hints:   ↔ wb 98   ∈ wcel 1393  [wsb 1645  {cab 2026

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-4 1400  ax-17 1419  ax-i9 1423

This theorem depends on definitions:  df-bi 110  df-sb 1646  df-clab 2027

This theorem is referenced by:  abeq2  2146  abeq2i  2148  abeq1i  2149  abeq2d  2150  abid2f  2202  elabgt  2684  elabgf  2685  ralab2  2705  rexab2  2707  sbccsbg  2878  sbccsb2g  2879  ss2ab  3008  abn0r  3243  tpid3g  3483  eluniab  3592  elintab  3626  iunab  3703  iinab  3718  intexabim  3906  iinexgm  3908  opm  3971  finds2  4324  dmmrnm  4554  sniota  4894  eusvobj2  5498  eloprabga  5591  indpi  6440  elabgf0  9916