Theorem abid 2718

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

Syntax hints:   ↔ wb 206  [wsb 2064   ∈ wcel 2108  {cab 2714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-12 2177

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715

This theorem is referenced by:  eqabbOLD  2882  eqabrd  2884  eqabf  2935  abid2fOLD  2937  elabgf  3674  ralab2  3703  rexab2  3705  ss2ab  4062  ab0ALT  4381  sbccsb  4436  sbccsb2  4437  eluniab  4921  elintabOLD  4959  iunab  5051  iinab  5068  zfrep4  5293  rnep  5937  sniota  6552  opabiota  6991  eusvobj2  7423  eloprabga  7542  finds2  7920  frrlem10  8320  wfrlem12OLD  8360  en3lplem2  9653  scottexs  9927  scott0s  9928  cp  9931  cardprclem  10019  cfflb  10299  fin23lem29  10381  axdc3lem2  10491  4sqlem12  16994  xkococn  23668  ptcmplem4  24063  noinfbnd1lem1  27768  ofpreima  32675  algextdeglem6  33763  qqhval2  33983  esum2dlem  34093  sigaclcu2  34121  bnj1143  34804  bnj1366  34843  bnj906  34944  bnj1256  35029  bnj1259  35030  bnj1311  35038  mclsax  35574  ellines  36153  bj-csbsnlem  36904  bj-reabeq  37028  bj-velpwALT  37054  topdifinffinlem  37348  rdgssun  37379  finxpreclem6  37397  finxpnom  37402  ralssiun  37408  setindtrs  43037  rababg  43587  scottabf  44259  compab  44461  tpid3gVD  44862  en3lplem2VD  44864  iunmapsn  45222  ssfiunibd  45321  absnsb  47039  setrec2lem2  49213