Theorem abid2 2873

Description: A simplification of class abstraction. Commuted form of abid1 2872. 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 2872	. 2 ⊢ 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴}
2	1	eqcomi 2745	1 ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴

Syntax hints:   = wceq 1541   ∈ wcel 2113  {cab 2714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811

This theorem is referenced by:  csbid  3862  csbconstg  3868  csbie  3884  abss  4014  ssab  4015  abssi  4020  notab  4266  dfrab3  4271  notrab  4274  eusn  4687  uniintsn  4940  axrep6g  5235  csbexg  5255  imai  6033  dffv4  6831  orduniss2  7775  dfixp  8837  euen1b  8965  modom2  9152  pwfir  9217  infmap2  10127  ustfn  24146  ustn0  24165  lrrecse  27938  lrrecpred  27940  fpwrelmap  32812  eulerpartlemgvv  34533  ballotlem2  34646  dffv5  36116  ptrest  37820  cnambfre  37869  cnvepresex  38531  pmapglb  40040  polval2N  40176  rngunsnply  43421  iocinico  43464