Theorem abid 2165

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

Syntax hints:   ↔ wb 105  [wsb 1762   ∈ wcel 2148  {cab 2163

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 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530

This theorem depends on definitions:  df-bi 117  df-sb 1763  df-clab 2164

This theorem is referenced by:  abeq2  2286  abeq2i  2288  abeq1i  2289  abeq2d  2290  abid2f  2345  elabgt  2879  elabgf  2880  ralab2  2902  rexab2  2904  sbccsbg  3087  sbccsb2g  3088  ss2ab  3224  abn0r  3448  abn0m  3449  tpid3g  3708  eluniab  3822  elintab  3856  iunab  3934  iinab  3949  intexabim  4153  iinexgm  4155  opm  4235  finds2  4601  dmmrnm  4847  sniota  5208  eusvobj2  5861  eloprabga  5962  indpi  7341  elabgf0  14532