Theorem abid 2163

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

Syntax hints:   ↔ wb 105  [wsb 1760   ∈ wcel 2146  {cab 2161

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 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-4 1508  ax-17 1524  ax-i9 1528

This theorem depends on definitions:  df-bi 117  df-sb 1761  df-clab 2162

This theorem is referenced by:  abeq2  2284  abeq2i  2286  abeq1i  2287  abeq2d  2288  abid2f  2343  elabgt  2876  elabgf  2877  ralab2  2899  rexab2  2901  sbccsbg  3084  sbccsb2g  3085  ss2ab  3221  abn0r  3445  abn0m  3446  tpid3g  3704  eluniab  3817  elintab  3851  iunab  3928  iinab  3943  intexabim  4147  iinexgm  4149  opm  4228  finds2  4594  dmmrnm  4839  sniota  5199  eusvobj2  5851  eloprabga  5952  indpi  7316  elabgf0  14089