Theorem abid 2226

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

Syntax hints:   ↔ wb 105  [wsb 1815   ∈ wcel 2209  {cab 2224

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 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583

This theorem depends on definitions:  df-bi 117  df-sb 1816  df-clab 2225

This theorem is referenced by:  abeq2  2347  abeq2i  2349  abeq1i  2350  abeq2d  2351  eqabrd  2378  abid2f  2418  elabgt  2967  elabgf  2968  ralab2  2990  rexab2  2992  sbccsbg  3176  sbccsb2g  3177  ss2ab  3316  abn0r  3546  abn0m  3547  tpid3g  3826  eluniab  3945  elintab  3979  iunab  4057  iinab  4072  intexabim  4286  iinexgm  4288  opm  4372  finds2  4746  dmmrnm  4999  iotaexab  5354  sniota  5366  eusvobj2  6065  eloprabga  6169  modom  7102  indpi  7703  4sqlem12  13164  elabgf0  16788