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

Syntax hints:   ↔ wb 205  [wsb 2067   ∈ wcel 2106  {cab 2715

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 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716

This theorem is referenced by:  abeq2  2872  abeq2d  2874  abbiOLD  2880  abid2f  2939  abeq2f  2940  elabgtOLD  3604  elabgf  3605  elabgOLD  3608  ralab2  3634  rexab2  3636  ss2ab  3993  ab0ALT  4310  abn0OLD  4315  sbccsb  4367  sbccsb2  4368  eluniab  4854  elintab  4890  iunab  4981  iinab  4997  zfrep4  5220  rnep  5836  sniota  6424  opabiota  6851  eusvobj2  7268  eloprabga  7382  eloprabgaOLD  7383  finds2  7747  frrlem10  8111  wfrlem12OLD  8151  en3lplem2  9371  scottexs  9645  scott0s  9646  cp  9649  cardprclem  9737  cfflb  10015  fin23lem29  10097  axdc3lem2  10207  4sqlem12  16657  xkococn  22811  ptcmplem4  23206  ofpreima  31002  qqhval2  31932  esum2dlem  32060  sigaclcu2  32088  bnj1143  32770  bnj1366  32809  bnj906  32910  bnj1256  32995  bnj1259  32996  bnj1311  33004  mclsax  33531  noinfbnd1lem1  33926  ellines  34454  bj-csbsnlem  35088  bj-reabeq  35217  topdifinffinlem  35518  rdgssun  35549  finxpreclem6  35567  finxpnom  35572  ralssiun  35578  setindtrs  40847  rababg  41181  scottabf  41858  compab  42060  tpid3gVD  42462  en3lplem2VD  42464  iunmapsn  42757  ssfiunibd  42848  absnsb  44521  setrec2lem2  46400