Theorem abid 2217

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

Syntax hints:   ↔ wb 105  [wsb 1808   ∈ wcel 2200  {cab 2215

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 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-4 1556  ax-17 1572  ax-i9 1576

This theorem depends on definitions:  df-bi 117  df-sb 1809  df-clab 2216

This theorem is referenced by:  abeq2  2338  abeq2i  2340  abeq1i  2341  abeq2d  2342  abid2f  2398  elabgt  2944  elabgf  2945  ralab2  2967  rexab2  2969  sbccsbg  3153  sbccsb2g  3154  ss2ab  3292  abn0r  3516  abn0m  3517  tpid3g  3781  eluniab  3899  elintab  3933  iunab  4011  iinab  4026  intexabim  4235  iinexgm  4237  opm  4319  finds2  4690  dmmrnm  4939  iotaexab  5293  sniota  5305  eusvobj2  5980  eloprabga  6082  indpi  7517  4sqlem12  12911  elabgf0  16071