Theorem abid 2742

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

This proof depends on syntax axioms:   ↔ wb 209  [wsb 2098   ∈ wcel 2144  {cab 2738

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739

This theorem is used by:  eqabrd  2901  eqabf  2951  abid2fOLD  2953  elabgf  3627  ralab2  3654  rexab2  3656  ss2ab  3986  ab0ALT  4329  sbccsb  4393  sbccsb2  4394  eluniab  4880  iunab  5009  iinab  5025  zfrep4  5245  rnep  5908  sniota  6530  opabiota  6968  eusvobj2  7413  eloprabga  7530  finds2  7911  ovmptss  8105  frrlem10  8317  en3lplem2  9618  scottabf  9943  scottexsOLD  9947  scott0bsOLD  9949  cp  9958  setrec2lem2  9980  cardprclem  10064  cfflb  10341  fin23lem29  10423  axdc3lem2  10533  4sqlem12  17140  xkococn  23985  ptcmplem4  24380  noinfbnd1lem1  28086  ofpreima  33307  algextdeglem6  34401  qqhval2  34661  esum2dlem  34771  sigaclcu2  34799  bnj1143  35467  bnj1366  35506  bnj906  35607  bnj1256  35692  bnj1259  35693  bnj1311  35701  mclsax  36421  ellines  37010  bj-csbsnlem  37908  bj-reabeq  38033  bj-velpwALT  38061  topdifinffinlem  38364  rdgssun  38395  finxpreclem6  38413  finxpnom  38418  ralssiun  38424  setindtrs  44126  rababg  44669  compab  45519  tpid3gVD  45918  en3lplem2VD  45920  permaxrep  46090  iunmapsn  46324  ssfiunibd  46419  absnsb  48191