Theorem abid 2341

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

Assertion

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

Proof of Theorem abid

Step	Hyp	Ref	Expression
1		df-clab 2340	. 2 ⊢ (x ∈ {x ∣ φ} ↔ [x / x]φ)
2		sbid 1922	. 2 ⊢ ([x / x]φ ↔ φ)
3	1, 2	bitri 240	1 ⊢ (x ∈ {x ∣ φ} ↔ φ)

Syntax hints:   ↔ wb 176  [wsb 1648   ∈ wcel 1710  {cab 2339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-sb 1649  df-clab 2340

This theorem is referenced by:  abeq2  2459  abeq2i  2461  abeq1i  2462  abeq2d  2463  abid2f  2515  elabgt  2983  elabgf  2984  ralab2  3002  rexab2  3004  sbccsbg  3165  sbccsb2g  3166  ss2ab  3335  abn0  3569  tpid3g  3832  eluniab  3904  elintab  3938  iunab  4013  iinab  4028  sniota  4370  eqop  4612  dfswap2  4742  eloprabga  5579