Theorem abid2 2863

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

Syntax hints:   = wceq 1533   ∈ wcel 2098  {cab 2702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802

This theorem is referenced by:  csbid  3903  csbconstg  3909  csbie  3926  abss  4055  ssab  4056  abssi  4064  notab  4304  dfrab3  4309  notrab  4312  eusn  4735  uniintsn  4990  iunidOLD  5064  axrep6g  5293  csbexg  5310  imai  6077  dffv4  6891  orduniss2  7835  dfixp  8916  euen1b  9050  pwfir  9199  modom2  9268  infmap2  10241  cshwsexaOLD  14807  ustfn  24136  ustn0  24155  lrrecse  27889  lrrecpred  27891  fpwrelmap  32572  eulerpartlemgvv  34066  ballotlem2  34178  dffv5  35590  ptrest  37162  cnambfre  37211  cnvepresex  37875  pmapglb  39312  polval2N  39448  rngunsnply  42662  iocinico  42705