Theorem abid 2220

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

Syntax hints:   ↔ wb 105  [wsb 1811   ∈ wcel 2203  {cab 2218

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 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579

This theorem depends on definitions:  df-bi 117  df-sb 1812  df-clab 2219

This theorem is referenced by:  abeq2  2341  abeq2i  2343  abeq1i  2344  abeq2d  2345  eqabrd  2370  abid2f  2410  elabgt  2957  elabgf  2958  ralab2  2980  rexab2  2982  sbccsbg  3166  sbccsb2g  3167  ss2ab  3305  abn0r  3532  abn0m  3533  tpid3g  3806  eluniab  3925  elintab  3959  iunab  4037  iinab  4052  intexabim  4263  iinexgm  4265  opm  4349  finds2  4722  dmmrnm  4975  iotaexab  5330  sniota  5342  eusvobj2  6035  eloprabga  6139  modom  7060  indpi  7656  4sqlem12  13096  elabgf0  16541