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  3753  eluniab  3868  elintab  3902  iunab  3980  iinab  3995  intexabim  4204  iinexgm  4206  opm  4286  finds2  4657  dmmrnm  4906  iotaexab  5259  sniota  5271  eusvobj2  5943  eloprabga  6045  indpi  7475  4sqlem12  12800  elabgf0  15852