Theorem abid 2748

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

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

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 2216

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

This theorem is used by:  eqabrd  2907  eqabf  2957  abid2fOLD  2959  elabgf  3636  ralab2  3663  rexab2  3665  ss2ab  4018  ab0ALT  4340  sbccsb  4404  sbccsb2  4405  eluniab  4891  iunab  5021  iinab  5037  zfrep4  5259  rnep  5922  sniota  6534  opabiota  6970  eusvobj2  7415  eloprabga  7532  finds2  7904  frrlem10  8301  en3lplem2  9592  scottabf  9878  scottexsOLD  9882  scott0bsOLD  9884  cp  9893  cardprclem  9984  cfflb  10261  fin23lem29  10343  axdc3lem2  10453  4sqlem12  17041  xkococn  23854  ptcmplem4  24249  noinfbnd1lem1  27924  ofpreima  33047  algextdeglem6  34143  qqhval2  34403  esum2dlem  34513  sigaclcu2  34541  bnj1143  35210  bnj1366  35249  bnj906  35350  bnj1256  35435  bnj1259  35436  bnj1311  35444  mclsax  36082  ellines  36665  bj-csbsnlem  37579  bj-reabeq  37704  bj-velpwALT  37730  topdifinffinlem  38034  rdgssun  38065  finxpreclem6  38083  finxpnom  38088  ralssiun  38094  setindtrs  43793  rababg  44341  compab  45192  tpid3gVD  45591  en3lplem2VD  45593  permaxrep  45756  iunmapsn  45974  ssfiunibd  46069  absnsb  47805  setrec2lem2  50513