Theorem abid 2088

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

Syntax hints:   ↔ wb 104   ∈ wcel 1448  [wsb 1703  {cab 2086

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-4 1455  ax-17 1474  ax-i9 1478

This theorem depends on definitions:  df-bi 116  df-sb 1704  df-clab 2087

This theorem is referenced by:  abeq2  2208  abeq2i  2210  abeq1i  2211  abeq2d  2212  abid2f  2265  elabgt  2779  elabgf  2780  ralab2  2801  rexab2  2803  sbccsbg  2981  sbccsb2g  2982  ss2ab  3112  abn0r  3334  abn0m  3335  tpid3g  3585  eluniab  3695  elintab  3729  iunab  3806  iinab  3821  intexabim  4017  iinexgm  4019  opm  4094  finds2  4453  dmmrnm  4696  sniota  5051  eusvobj2  5692  eloprabga  5790  indpi  7051  elabgf0  12565