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  3631  ralab2  3657  rexab2  3659  ss2ab  4015  ab0ALT  4335  sbccsb  4390  sbccsb2  4391  eluniab  4879  iunab  5009  iinab  5025  zfrep4  5240  rnep  5884  sniota  6491  opabiota  6924  eusvobj2  7360  eloprabga  7477  finds2  7850  frrlem10  8247  en3lplem2  9534  scottexs  9811  scott0s  9812  cp  9815  cardprclem  9903  cfflb  10181  fin23lem29  10263  axdc3lem2  10373  4sqlem12  16896  xkococn  23616  ptcmplem4  24011  noinfbnd1lem1  27703  ofpreima  32754  algextdeglem6  33899  qqhval2  34159  esum2dlem  34269  sigaclcu2  34297  bnj1143  34965  bnj1366  35004  bnj906  35105  bnj1256  35190  bnj1259  35191  bnj1311  35199  mclsax  35782  ellines  36365  bj-csbsnlem  37148  bj-reabeq  37272  bj-velpwALT  37298  topdifinffinlem  37599  rdgssun  37630  finxpreclem6  37648  finxpnom  37653  ralssiun  37659  setindtrs  43379  rababg  43927  scottabf  44593  compab  44794  tpid3gVD  45194  en3lplem2VD  45196  permaxrep  45359  iunmapsn  45572  ssfiunibd  45668  absnsb  47384  setrec2lem2  50050