Theorem abid 2740

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

Syntax hints:   ↔ wb 196  [wsb 2038   ∈ wcel 2131  {cab 2738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-12 2188

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1846  df-sb 2039  df-clab 2739

This theorem is referenced by:  abeq2  2862  abeq2d  2864  abbi  2867  abid2f  2921  abeq2f  2922  elabgt  3479  elabgf  3480  ralab2  3504  rexab2  3506  ss2ab  3803  ab0  4086  abn0  4089  sbccsb  4139  sbccsb2  4140  eluniab  4591  elintab  4631  iunab  4710  iinab  4725  zfrep4  4923  sniota  6031  opabiota  6415  eusvobj2  6798  eloprabga  6904  finds2  7251  wfrlem12  7587  en3lplem2  8673  scottexs  8915  scott0s  8916  cp  8919  cardprclem  8987  cfflb  9265  fin23lem29  9347  axdc3lem2  9457  4sqlem12  15854  xkococn  21657  ptcmplem4  22052  ofpreima  29766  qqhval2  30327  esum2dlem  30455  sigaclcu2  30484  bnj1143  31160  bnj1366  31199  bnj906  31299  bnj1256  31382  bnj1259  31383  bnj1311  31391  mclsax  31765  ellines  32557  bj-abeq2  33071  bj-csbsnlem  33196  topdifinffinlem  33498  finxpreclem6  33536  finxpnom  33541  setindtrs  38086  rababg  38373  compab  39139  tpid3gVD  39568  en3lplem2VD  39570  iunmapsn  39900  ssfiunibd  40014  setrec2lem2  42943