Theorem abid 2744

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

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

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 2215

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

This theorem is used by:  eqabrd  2903  eqabf  2953  abid2fOLD  2955  elabgf  3631  ralab2  3658  rexab2  3660  ss2ab  4012  ab0ALT  4333  sbccsb  4397  sbccsb2  4398  eluniab  4884  iunab  5014  iinab  5030  zfrep4  5252  rnep  5915  sniota  6528  opabiota  6964  eusvobj2  7409  eloprabga  7526  finds2  7899  frrlem10  8298  en3lplem2  9596  scottabf  9882  scottexsOLD  9886  scott0bsOLD  9888  cp  9897  cardprclem  9988  cfflb  10265  fin23lem29  10347  axdc3lem2  10457  4sqlem12  17054  xkococn  23892  ptcmplem4  24287  noinfbnd1lem1  27967  ofpreima  33146  algextdeglem6  34240  qqhval2  34500  esum2dlem  34610  sigaclcu2  34638  bnj1143  35307  bnj1366  35346  bnj906  35447  bnj1256  35532  bnj1259  35533  bnj1311  35541  mclsax  36156  ellines  36740  bj-csbsnlem  37654  bj-reabeq  37779  bj-velpwALT  37805  topdifinffinlem  38109  rdgssun  38140  finxpreclem6  38158  finxpnom  38163  ralssiun  38169  setindtrs  43874  rababg  44422  compab  45273  tpid3gVD  45672  en3lplem2VD  45674  permaxrep  45837  iunmapsn  46055  ssfiunibd  46150  absnsb  47923  setrec2lem2  50628