Theorem abid 2128

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

Syntax hints:   ↔ wb 104   ∈ wcel 1481  [wsb 1736  {cab 2126

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-4 1488  ax-17 1507  ax-i9 1511

This theorem depends on definitions:  df-bi 116  df-sb 1737  df-clab 2127

This theorem is referenced by:  abeq2  2249  abeq2i  2251  abeq1i  2252  abeq2d  2253  abid2f  2307  elabgt  2829  elabgf  2830  ralab2  2852  rexab2  2854  sbccsbg  3036  sbccsb2g  3037  ss2ab  3170  abn0r  3392  abn0m  3393  tpid3g  3646  eluniab  3756  elintab  3790  iunab  3867  iinab  3882  intexabim  4085  iinexgm  4087  opm  4164  finds2  4523  dmmrnm  4766  sniota  5123  eusvobj2  5768  eloprabga  5866  indpi  7174  elabgf0  13155