Theorem abid 2181

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

Syntax hints:   ↔ wb 105  [wsb 1773   ∈ wcel 2164  {cab 2179

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 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-4 1521  ax-17 1537  ax-i9 1541

This theorem depends on definitions:  df-bi 117  df-sb 1774  df-clab 2180

This theorem is referenced by:  abeq2  2302  abeq2i  2304  abeq1i  2305  abeq2d  2306  abid2f  2362  elabgt  2901  elabgf  2902  ralab2  2924  rexab2  2926  sbccsbg  3109  sbccsb2g  3110  ss2ab  3247  abn0r  3471  abn0m  3472  tpid3g  3733  eluniab  3847  elintab  3881  iunab  3959  iinab  3974  intexabim  4181  iinexgm  4183  opm  4263  finds2  4633  dmmrnm  4881  iotaexab  5233  sniota  5245  eusvobj2  5904  eloprabga  6005  indpi  7402  4sqlem12  12540  elabgf0  15269