Theorem abid 2719

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

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

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 2716

This theorem is referenced by:  eqabrd  2878  eqabf  2929  abid2fOLD  2931  elabgf  3618  ralab2  3644  rexab2  3646  ss2ab  4002  ab0ALT  4322  sbccsb  4377  sbccsb2  4378  eluniab  4865  iunab  4995  iinab  5011  zfrep4  5228  rnep  5876  sniota  6483  opabiota  6916  eusvobj2  7352  eloprabga  7469  finds2  7842  frrlem10  8238  en3lplem2  9525  scottexs  9802  scott0s  9803  cp  9806  cardprclem  9894  cfflb  10172  fin23lem29  10254  axdc3lem2  10364  4sqlem12  16918  xkococn  23635  ptcmplem4  24030  noinfbnd1lem1  27701  ofpreima  32753  algextdeglem6  33882  qqhval2  34142  esum2dlem  34252  sigaclcu2  34280  bnj1143  34948  bnj1366  34987  bnj906  35088  bnj1256  35173  bnj1259  35174  bnj1311  35182  mclsax  35767  ellines  36350  bj-csbsnlem  37226  bj-reabeq  37350  bj-velpwALT  37376  topdifinffinlem  37677  rdgssun  37708  finxpreclem6  37726  finxpnom  37731  ralssiun  37737  setindtrs  43471  rababg  44019  scottabf  44685  compab  44886  tpid3gVD  45286  en3lplem2VD  45288  permaxrep  45451  iunmapsn  45664  ssfiunibd  45760  absnsb  47487  setrec2lem2  50181