Theorem abid 2184

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

Syntax hints:   ↔ wb 105  [wsb 1776   ∈ wcel 2167  {cab 2182

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 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-4 1524  ax-17 1540  ax-i9 1544

This theorem depends on definitions:  df-bi 117  df-sb 1777  df-clab 2183

This theorem is referenced by:  abeq2  2305  abeq2i  2307  abeq1i  2308  abeq2d  2309  abid2f  2365  elabgt  2905  elabgf  2906  ralab2  2928  rexab2  2930  sbccsbg  3113  sbccsb2g  3114  ss2ab  3251  abn0r  3475  abn0m  3476  tpid3g  3737  eluniab  3851  elintab  3885  iunab  3963  iinab  3978  intexabim  4185  iinexgm  4187  opm  4267  finds2  4637  dmmrnm  4885  iotaexab  5237  sniota  5249  eusvobj2  5908  eloprabga  6009  indpi  7409  4sqlem12  12571  elabgf0  15423