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

Syntax hints:   ↔ wb 206  [wsb 2068   ∈ wcel 2114  {cab 2714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

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

This theorem is referenced by:  eqabrd  2877  eqabf  2928  abid2fOLD  2930  elabgf  3617  ralab2  3643  rexab2  3645  ss2ab  4001  ab0ALT  4321  sbccsb  4376  sbccsb2  4377  eluniab  4864  iunab  4994  iinab  5010  zfrep4  5228  rnep  5882  sniota  6489  opabiota  6922  eusvobj2  7359  eloprabga  7476  finds2  7849  frrlem10  8245  en3lplem2  9534  scottexs  9811  scott0s  9812  cp  9815  cardprclem  9903  cfflb  10181  fin23lem29  10263  axdc3lem2  10373  4sqlem12  16927  xkococn  23625  ptcmplem4  24020  noinfbnd1lem1  27687  ofpreima  32738  algextdeglem6  33866  qqhval2  34126  esum2dlem  34236  sigaclcu2  34264  bnj1143  34932  bnj1366  34971  bnj906  35072  bnj1256  35157  bnj1259  35158  bnj1311  35166  mclsax  35751  ellines  36334  bj-csbsnlem  37210  bj-reabeq  37334  bj-velpwALT  37360  topdifinffinlem  37663  rdgssun  37694  finxpreclem6  37712  finxpnom  37717  ralssiun  37723  setindtrs  43453  rababg  44001  scottabf  44667  compab  44868  tpid3gVD  45268  en3lplem2VD  45270  permaxrep  45433  iunmapsn  45646  ssfiunibd  45742  absnsb  47475  setrec2lem2  50169