Theorem abid 2194

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

Syntax hints:   ↔ wb 105  [wsb 1786   ∈ wcel 2177  {cab 2192

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 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-4 1534  ax-17 1550  ax-i9 1554

This theorem depends on definitions:  df-bi 117  df-sb 1787  df-clab 2193

This theorem is referenced by:  abeq2  2315  abeq2i  2317  abeq1i  2318  abeq2d  2319  abid2f  2375  elabgt  2918  elabgf  2919  ralab2  2941  rexab2  2943  sbccsbg  3126  sbccsb2g  3127  ss2ab  3265  abn0r  3489  abn0m  3490  tpid3g  3752  eluniab  3867  elintab  3901  iunab  3979  iinab  3994  intexabim  4203  iinexgm  4205  opm  4285  finds2  4656  dmmrnm  4905  iotaexab  5258  sniota  5270  eusvobj2  5942  eloprabga  6044  indpi  7470  4sqlem12  12795  elabgf0  15847