Theorem abid 2219

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

Syntax hints:   ↔ wb 105  [wsb 1810   ∈ wcel 2202  {cab 2217

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 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578

This theorem depends on definitions:  df-bi 117  df-sb 1811  df-clab 2218

This theorem is referenced by:  abeq2  2340  abeq2i  2342  abeq1i  2343  abeq2d  2344  abid2f  2400  elabgt  2947  elabgf  2948  ralab2  2970  rexab2  2972  sbccsbg  3156  sbccsb2g  3157  ss2ab  3295  abn0r  3519  abn0m  3520  tpid3g  3787  eluniab  3905  elintab  3939  iunab  4017  iinab  4032  intexabim  4242  iinexgm  4244  opm  4326  finds2  4699  dmmrnm  4951  iotaexab  5305  sniota  5317  eusvobj2  6004  eloprabga  6108  modom  6994  indpi  7562  4sqlem12  12980  elabgf0  16399