Theorem abid2 2899

Description: A simplification of class abstraction. Commuted form of abid1 2898. See comments there. (Contributed by NM, 26-Dec-1993.)

Assertion

Ref	Expression
abid2	⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴

Distinct variable group:   𝑥,𝐴

Proof of Theorem abid2

Step	Hyp	Ref	Expression
1		abid1 2898	. 2 ⊢ 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴}
2	1	eqcomi 2771	1 ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴

Syntax hints:   = wceq 1560   ∈ wcel 2142  {cab 2740

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837

This theorem is referenced by:  csbid  3865  csbconstg  3871  csbie  3887  abss  4015  ssab  4016  abssi  4021  notab  4266  dfrab3  4271  notrab  4274  eusn  4689  uniintsn  4943  axrep6g  5240  csbexg  5260  imai  6063  dffv4  6864  orduniss2  7813  dfixp  8881  euen1b  9009  modom2  9196  pwfir  9261  infmap2  10173  ustfn  24262  ustn0  24281  lrrecse  28035  lrrecpred  28037  fpwrelmap  32935  eulerpartlemgvv  34673  ballotlem2  34786  dffv5  36272  ptrest  38118  cnambfre  38167  cnvepresex  38835  pmapglb  40394  polval2N  40530  rngunsnply  43746  iocinico  43789