Theorem abid 2219

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

Syntax hints:   ↔ wb 105  [wsb 1810   ∈ wcel 2202  {cab 2217

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 1811  df-clab 2218

This theorem is referenced by:  abeq2  2340  abeq2i  2342  abeq1i  2343  abeq2d  2344  abid2f  2401  elabgt  2948  elabgf  2949  ralab2  2971  rexab2  2973  sbccsbg  3157  sbccsb2g  3158  ss2ab  3296  abn0r  3521  abn0m  3522  tpid3g  3791  eluniab  3910  elintab  3944  iunab  4022  iinab  4037  intexabim  4247  iinexgm  4249  opm  4332  finds2  4705  dmmrnm  4957  iotaexab  5312  sniota  5324  eusvobj2  6014  eloprabga  6118  modom  7037  indpi  7605  4sqlem12  13036  elabgf0  16475