Theorem abid 2714

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

Syntax hints:   ↔ wb 205  [wsb 2068   ∈ wcel 2107  {cab 2710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711

This theorem is referenced by:  eqabbOLD  2875  eqabrd  2877  eqabf  2936  abid2fOLD  2938  elabgtOLD  3664  elabgf  3665  elabgOLD  3668  ralab2  3694  rexab2  3696  ss2ab  4057  ab0ALT  4377  abn0OLD  4382  sbccsb  4434  sbccsb2  4435  eluniab  4924  elintabOLD  4964  iunab  5055  iinab  5072  zfrep4  5297  rnep  5927  sniota  6535  opabiota  6975  eusvobj2  7401  eloprabga  7516  eloprabgaOLD  7517  finds2  7891  frrlem10  8280  wfrlem12OLD  8320  en3lplem2  9608  scottexs  9882  scott0s  9883  cp  9886  cardprclem  9974  cfflb  10254  fin23lem29  10336  axdc3lem2  10446  4sqlem12  16889  xkococn  23164  ptcmplem4  23559  noinfbnd1lem1  27226  ofpreima  31890  qqhval2  32962  esum2dlem  33090  sigaclcu2  33118  bnj1143  33801  bnj1366  33840  bnj906  33941  bnj1256  34026  bnj1259  34027  bnj1311  34035  mclsax  34560  ellines  35124  bj-csbsnlem  35783  bj-reabeq  35908  bj-velpwALT  35934  topdifinffinlem  36228  rdgssun  36259  finxpreclem6  36277  finxpnom  36282  ralssiun  36288  setindtrs  41764  rababg  42325  scottabf  42999  compab  43201  tpid3gVD  43603  en3lplem2VD  43605  iunmapsn  43916  ssfiunibd  44019  absnsb  45737  setrec2lem2  47739