Theorem abid 2715

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

Syntax hints:   ↔ wb 206  [wsb 2067   ∈ wcel 2113  {cab 2711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2182

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712

This theorem is referenced by:  eqabrd  2874  eqabf  2925  abid2fOLD  2927  elabgf  3626  ralab2  3652  rexab2  3654  ss2ab  4010  ab0ALT  4330  sbccsb  4385  sbccsb2  4386  eluniab  4872  iunab  5002  iinab  5018  zfrep4  5233  rnep  5871  sniota  6477  opabiota  6910  eusvobj2  7344  eloprabga  7461  finds2  7834  frrlem10  8231  en3lplem2  9510  scottexs  9787  scott0s  9788  cp  9791  cardprclem  9879  cfflb  10157  fin23lem29  10239  axdc3lem2  10349  4sqlem12  16870  xkococn  23576  ptcmplem4  23971  noinfbnd1lem1  27663  ofpreima  32649  algextdeglem6  33756  qqhval2  34016  esum2dlem  34126  sigaclcu2  34154  bnj1143  34823  bnj1366  34862  bnj906  34963  bnj1256  35048  bnj1259  35049  bnj1311  35057  mclsax  35634  ellines  36217  bj-csbsnlem  36968  bj-reabeq  37092  bj-velpwALT  37118  topdifinffinlem  37412  rdgssun  37443  finxpreclem6  37461  finxpnom  37466  ralssiun  37472  setindtrs  43143  rababg  43692  scottabf  44358  compab  44559  tpid3gVD  44959  en3lplem2VD  44961  permaxrep  45124  iunmapsn  45339  ssfiunibd  45435  absnsb  47152  setrec2lem2  49820