Theorem abid 2125

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

Syntax hints:   ↔ wb 104   ∈ wcel 1480  [wsb 1735  {cab 2123

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 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-4 1487  ax-17 1506  ax-i9 1510

This theorem depends on definitions:  df-bi 116  df-sb 1736  df-clab 2124

This theorem is referenced by:  abeq2  2246  abeq2i  2248  abeq1i  2249  abeq2d  2250  abid2f  2304  elabgt  2820  elabgf  2821  ralab2  2843  rexab2  2845  sbccsbg  3026  sbccsb2g  3027  ss2ab  3160  abn0r  3382  abn0m  3383  tpid3g  3633  eluniab  3743  elintab  3777  iunab  3854  iinab  3869  intexabim  4072  iinexgm  4074  opm  4151  finds2  4510  dmmrnm  4753  sniota  5110  eusvobj2  5753  eloprabga  5851  indpi  7143  elabgf0  12973