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  3252  abn0r  3476  abn0m  3477  tpid3g  3738  eluniab  3852  elintab  3886  iunab  3964  iinab  3979  intexabim  4186  iinexgm  4188  opm  4268  finds2  4638  dmmrnm  4886  iotaexab  5238  sniota  5250  eusvobj2  5911  eloprabga  6013  indpi  7426  4sqlem12  12596  elabgf0  15507