Theorem abid 2779

Description: Simplification of class abstraction notation when the free and bound variables are identical. (Contributed by NM, 26-May-1993.)

Assertion

Ref	Expression
abid	⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)

Proof of Theorem abid

Step	Hyp	Ref	Expression
1		df-clab 2776	. 2 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ [𝑥 / 𝑥]𝜑)
2		sbid 2220	. 2 ⊢ ([𝑥 / 𝑥]𝜑 ↔ 𝜑)
3	1, 2	bitri 276	1 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)

Syntax hints:   ↔ wb 207  [wsb 2042   ∈ wcel 2081  {cab 2775

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-12 2141

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-sb 2043  df-clab 2776

This theorem is referenced by:  abeq2  2914  abeq2d  2916  abbi  2924  abid2f  2980  abeq2f  2981  abeq2fOLD  2982  elabgt  3601  elabgf  3602  elabg  3604  ralab2  3626  rexab2  3628  ss2ab  3960  ab0  4253  abn0  4256  sbccsb  4300  sbccsb2  4301  eluniab  4756  elintab  4793  iunab  4874  iinab  4889  zfrep4  5091  sniota  6216  opabiota  6613  eusvobj2  7009  eloprabga  7117  finds2  7466  wfrlem12  7818  en3lplem2  8922  scottexs  9162  scott0s  9163  cp  9166  cardprclem  9254  cfflb  9527  fin23lem29  9609  axdc3lem2  9719  4sqlem12  16121  xkococn  21952  ptcmplem4  22347  ofpreima  30100  qqhval2  30840  esum2dlem  30968  sigaclcu2  30996  bnj1143  31679  bnj1366  31718  bnj906  31818  bnj1256  31901  bnj1259  31902  bnj1311  31910  mclsax  32424  frrlem10  32741  ellines  33222  bj-abeq2  33690  bj-csbsnlem  33791  topdifinffinlem  34159  rdgssun  34190  finxpreclem6  34208  finxpnom  34213  ralssiun  34219  setindtrs  39107  rababg  39418  scottabf  40073  compab  40313  tpid3gVD  40715  en3lplem2VD  40717  iunmapsn  41020  ssfiunibd  41117  absnsb  42778  setrec2lem2  44277