Theorem abid 2222

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

Syntax hints:   ↔ wb 105  [wsb 1811   ∈ wcel 2205  {cab 2220

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 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579

This theorem depends on definitions:  df-bi 117  df-sb 1812  df-clab 2221

This theorem is referenced by:  abeq2  2343  abeq2i  2345  abeq1i  2346  abeq2d  2347  eqabrd  2372  abid2f  2412  elabgt  2961  elabgf  2962  ralab2  2984  rexab2  2986  sbccsbg  3170  sbccsb2g  3171  ss2ab  3310  abn0r  3537  abn0m  3538  tpid3g  3812  eluniab  3931  elintab  3965  iunab  4043  iinab  4058  intexabim  4269  iinexgm  4271  opm  4355  finds2  4728  dmmrnm  4981  iotaexab  5336  sniota  5348  eusvobj2  6044  eloprabga  6148  modom  7074  indpi  7673  4sqlem12  13125  elabgf0  16661