Theorem abid 2743

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

This proof depends on syntax axioms:   ↔ wb 209  [wsb 2099   ∈ wcel 2145  {cab 2739

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2213

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740

This theorem is used by:  eqabrd  2902  eqabf  2952  abid2fOLD  2954  elabgf  3628  ralab2  3655  rexab2  3657  ss2ab  4009  ab0ALT  4330  sbccsb  4394  sbccsb2  4395  eluniab  4881  iunab  5010  iinab  5026  zfrep4  5246  rnep  5909  sniota  6522  opabiota  6959  eusvobj2  7404  eloprabga  7521  finds2  7899  frrlem10  8297  en3lplem2  9598  scottabf  9920  scottexsOLD  9924  scott0bsOLD  9926  cp  9935  setrec2lem2  9957  cardprclem  10041  cfflb  10318  fin23lem29  10400  axdc3lem2  10510  4sqlem12  17114  xkococn  23959  ptcmplem4  24354  noinfbnd1lem1  28062  ofpreima  33241  algextdeglem6  34336  qqhval2  34596  esum2dlem  34706  sigaclcu2  34734  bnj1143  35403  bnj1366  35442  bnj906  35543  bnj1256  35628  bnj1259  35629  bnj1311  35637  mclsax  36303  ellines  36887  bj-csbsnlem  37785  bj-reabeq  37910  bj-velpwALT  37936  topdifinffinlem  38238  rdgssun  38269  finxpreclem6  38287  finxpnom  38292  ralssiun  38298  setindtrs  43985  rababg  44533  compab  45384  tpid3gVD  45783  en3lplem2VD  45785  permaxrep  45948  iunmapsn  46173  ssfiunibd  46268  absnsb  48041